diff --git a/tex/macros.tex b/tex/macros.tex
new file mode 100644
index 0000000000000000000000000000000000000000..eab355e3bb148d02172b9e816b47471ed0d7e318
--- /dev/null
+++ b/tex/macros.tex
@@ -0,0 +1,22 @@
+\newcommand{\bnf}[1]{{\color{red}#1}}
+\newcommand{\type}{\mathtt{type}}
+\newcommand{\kind}{\mathtt{kind}}
+\newcommand{\self}{\mathtt{self}}
+\newcommand{\judg}[2]{#1 \vdash #2}
+\newcommand{\gjudg}[1]{\judg\Gamma{#1}}
+\newcommand{\tjudg}[2]{\judg{\Theta;#1}{#2}}
+\newcommand{\tgjudg}[1]{\tjudg{\Gamma}{#1}}
+\newcommand{\hastype}[2]{ #1 : #2 }
+\newcommand{\judgeq}[3]{ #1 \equiv #2:#3}
+\newcommand{\judgeqc}[2]{ #1 \rewrites #2}
+\newcommand{\oma}[2]{\ensuremath{@\left( #1, #2 \right)}}
+\newcommand{\ombind}[3]{\ensuremath{\beta\left( #1 \left\{ #2 \right\} #3 \right)}}
+
+\newcommand{\incl}[1]{\mathtt{include}\,#1}
+\newcommand{\gray}[1]{{\color{gray}#1}}
+\newcommand{\red}[1]{{\color{red}#1}}
+
+\newcommand{\cn}[1]{\ensuremath{\mathtt{#1}}}
+\def\defemph{\textbf}
+
+
diff --git a/tex/paper.tex b/tex/paper.tex
index 3f567a35a504789f070999d2aa01e15acc1e5d15..4d1b2bed4db7f967e458b98b62640acdfe9395d0 100644
--- a/tex/paper.tex
+++ b/tex/paper.tex
@@ -1,7 +1,7 @@
 \documentclass[orivec]{llncs}
 
 \usepackage[utf8]{inputenc}
-\usepackage{url}
+\usepackage{url, multirow}
 %\usepackage{tipa}
 \usepackage{amsmath,amssymb,amstext}
 \usepackage{graphicx,stmaryrd,mathabx,MnSymbol,tabularx,mathtools}
@@ -61,6 +61,8 @@
 \author{Dennis Müller\inst{1} \and Michael Kohlhase\inst{1}\and Florian Rabe\inst{1,2}}
 \institute{Computer Science, FAU Erlangen-N\"urnberg\and LRI, Universit\'e Paris Sud}
 
+\input{macros}
+
 \begin{document}
 
 %\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
diff --git a/tex/prelim.tex b/tex/prelim.tex
index 6b559dca6a57199097930966ff1a41723dd7ae84..0dafe61280b4944892c5e46ba87b02b050de855d 100644
--- a/tex/prelim.tex
+++ b/tex/prelim.tex
@@ -1 +1,48 @@
-MMT theories, flat, bla
\ No newline at end of file
+MMT theories, flat, bla
+
+\subsection{MMT Grammar}
+
+For the purposes of this paper, we will work with the (only slightly simplified) grammar given in Figure \ref{fig:mmtgrammar}.
+
+\begin{figure}[ht]\centering\vspace*{-1em}
+  \begin{mdframed}
+    \begin{tabular}{rl@{\quad}l|l}
+      \cn{Thy} 	$::=$ 	& $T[:T]=\{ (\cn{Inc})^\ast\ (\cn{Const})^\ast \}$	& Theory				& \multirow{2}{*}{Modules} \\
+      \cn{View} 	$::=$	& $T : T \to T = \{ (\cn{Ass})^\ast \}$			& View 				& \\ \hline
+      \cn{Const} 	$::=$ 	& $C [:t] [=t]$ 								& Constant Declarations& \multirow{3}{*}{Declarations} \\
+      \cn{Inc}	$::=$	& $\incl T$								& Includes			& \\
+      \cn{Ass}	$::=$	& $C = t$									& Assignments		& \\ \hline
+      $\Gamma$	$::=$	& $(x [:t][=t])^\ast$						& Variable Contexts	& \multirow{2}{*}{Objects} \\
+      $t$ 		$::=$ 	& $x \mid T?C \mid \oma{t}{(t)^+} \mid \ombind{t}{\Gamma}{t} $		& Terms 	& \\\hline\hline
+      $T$		$::=$ 	& \cn{String}								& Module Names 		& \multirow{3}{*}{Strings} \\
+      $C$		$::=$ 	& \cn{String}								& Constant Names		& \\
+      $x$		$::=$ 	& \cn{String}								& Variable Names		& \\
+    \end{tabular}
+  \end{mdframed}\vspace*{-.5em}
+  \caption{The MMT Grammar}\label{fig:mmtgrammar}\label{fig:mmtgrammar}\vspace*{-1em}
+\end{figure}
+
+In more detail:
+\begin{itemize}
+	\item Theories have a module name, an optional \emph{meta-theory} and a body consisting of \emph{includes} of other theories
+		 and a list of \emph{constant declarations}.
+	\item Constant declarations have a name and two optional term components; a \emph{type} ($[:t]$), and a \emph{definition} ($[=t]$).
+	\item Views $V : T_1 \to T_2$ have a module name, a domain theory $T_1$, a codomain theory $T_2$ and a body consisting of assignments
+		$C = t$.
+	\item Terms are either 
+		\begin{itemize}
+			\item variables $x$, 
+			\item symbol references $T?C$ (referencing the constant $C$ in theory $T$), 
+			\item applications $\oma{f}{a_1,\ldots,a_n}$ of a term $f$ to a list of arguments $a_1,\ldots,a_n$ or
+			\item binding application $\ombind{f}{x_1[:t_1][=d_1],\ldots,x_n[:t_n][=d_n]}{b}$, where $f$ \emph{binds} the variables
+				$x_1,\ldots,x_n$ in the body $b$ (representing binders such as quantifiers, lambdas, dependent type constructors etc.).
+		\end{itemize}
+\end{itemize}
+The term components of a constant in a theory $T$ may only contain symbol references to constants declared previously in $T$, or that are declared in some theory $T'$ (recursively) included in $T$ (or its meta-theory, which we consider an \emph{include} as well). 
+We can eliminate all includes in a theory $T$ by simply copying over the constant declarations in the included theories; we call this process \emph{flattening}. We will often and without loss of generality assume a theory to be \emph{flat} for convenience.
+
+An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any assignment $C=t$ contained, $C$ is a constant declared in the flattened domain $T_1$ and $t$ is a syntactically well-formed term in the codomain $T_2$. We call a view \emph{total} if all \emph{undefined} constants in the domain have a corresponding assignment and \emph{partial} otherwise.
+
+\subsection{Theory Graphs and Library Encoding}
+
+OAF?, Meta-Theories, Logical Frameworks / LF, HOAS,  Judgments-as-Types
\ No newline at end of file