diff --git a/merkzettel.pdf b/merkzettel.pdf
index bdf2e6e..eec4f51 100644
Binary files a/merkzettel.pdf and b/merkzettel.pdf differ
diff --git a/merkzettel.tex b/merkzettel.tex
index ef9760e..7adb3fd 100644
--- a/merkzettel.tex
+++ b/merkzettel.tex
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{scrartcl}
-\usepackage[a4paper,left=1.5cm,right=3.0cm,top=2.5cm,bottom=2.5cm]{geometry}
+\usepackage[a4paper,left=3cm,right=3cm,top=2.5cm,bottom=2.5cm]{geometry}
 \usepackage[ngerman]{babel}
 \usepackage{amssymb}
 \usepackage{amsthm}
@@ -110,7 +110,9 @@
 	\item Subjektreduktion: Wenn $\Gamma\vdash t:\alpha$ und $t \rightarrow_\beta^* s$, dann auch $\Gamma \vdash s:\alpha$, aber nicht umgekehrt! \satz{3.38}{45}
 \end{itemize}
 \section*{Induktive Datentypen}
+\subsection*{Mengenkonstruktionen}
 \subsection*{Mehrsortigkeit}
+
 \subsection*{Strukturelle Induktion}
 \begin{itemize}
 \item über einsortige Datentypen \siehe{S. 63}
@@ -135,8 +137,61 @@
 \end{itemize}
 \subsection*{Kodatentypen mit Alternativen}
 \section*{System F}
-\section*{Polymorphie}
+\subsection*{Curry}
+\begin{itemize}
+	\item Typen:\defin{5.1}{84}
+	\begin{align*}
+	\alpha, \beta \coloneqq a\ \vert\ \alpha \rightarrow \beta\ \vert\ \forall a.\alpha && (a\in V)
+	\end{align*}
+	\item Typisierung: \textbf{TODO: $\lambda \rightarrow$}, \textbf{TODO} \defin{5.1}{84}
+	\begin{align*}
+	Inhalt...
+	\end{align*}
+\end{itemize}
+\subsection*{Church-Kodierung}\siehe{S. 84}
+\begin{itemize}
+	\item Natürliche Zahlen
+	\begin{align*}
+	\textbf{Todo}
+	\end{align*}
+	\item Paare
+	\begin{align*}
+	Inhalt...
+	\end{align*}
+	\item Summen
+	\begin{align*}
+	Inhalt...
+	\end{align*}
+	\item Listen
+	\begin{align*}
+	Inhalt...
+	\end{align*}
+\end{itemize}
 \subsection*{ML-Polymorphie}
+\begin{itemize}
+	\item Einschränkung von System F durch $\forall$ nur auf oberster Ebene sowie Mehrfachinstanziierung polymorpher Funktionen nur in $let$-Konstrukt \siehe{S. 88}
+	\item Typen
+	\begin{equation*}
+	\alpha, \beta \coloneqq a\ \vert\ \alpha \rightarrow \beta
+	\end{equation*}
+	\item Typschemata
+	\begin{align*}
+	S \coloneqq \forall a_1, \ldots, a_k.\alpha &&(k\geq 0)
+	\end{align*}
+	\item Terme
+	\begin{equation*}
+	t,s \coloneqq x\ \vert\ t\ s\ \vert\ \lambda x.t\ \vert\ let\ x = t\ in\ s
+	\end{equation*}
+	\item Kontexte
+	\begin{align*}
+		\Gamma &= ( x_1:S_1,\ldots, x_n :S_n )\\
+		Cl(\Gamma, \alpha) &= \forall a_1,\ldots,a_k.\alpha &&\text{für $FV(\alpha)\backslash FV(\Gamma) = \lbrace a_1,\ldots,a_k \rbrace$}
+	\end{align*}
+	\item Typisierungsregeln \textbf{TODO}
+	\item Inversionslemma \textbf{TODO}
+	\item erweiterter Algorithmus W \textbf{TODO}
+\end{itemize}
+\section*{Reguläre Ausdrücke}
 \section*{Unifikationsalgorithmus (Martelli/Montanari)}
 \begin{align*}
 &S \cup \lbrace x \pteq x\rbrace &&\rightarrow S &&\text{(delete)}\\