--- a/Slides/Slides5.thy	Wed Mar 30 08:11:36 2011 +0200
+++ b/Slides/Slides5.thy	Wed Mar 30 22:27:26 2011 +0200
@@ -11,6 +11,8 @@
 
 
 text_raw {*
+  %% shallow, deep, and recursive binders
+  %%
   %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
   %%\renewcommand{\slidecaption}{Uppsala, 3.~March 2011}
   \renewcommand{\slidecaption}{Saarbrücken, 31.~March 2011}
@@ -20,8 +22,10 @@
   \frametitle{%
   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
   \\
-  \huge General Bindings and Alpha-Equivalence in Nominal Isabelle\\[-2mm] 
-  \large Or, Nominal 2\\[-5mm]
+  \LARGE General Bindings and\\ 
+  \LARGE Alpha-Equivalence\\ 
+  \LARGE in Nominal Isabelle\\[3mm] 
+  \Large Or, Nominal Isabelle 2\\[-5mm]
   \end{tabular}}
   \begin{center}
   Christian Urban
@@ -73,6 +77,22 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-2>
+  \frametitle{New Types in HOL}
+
+  picture
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -211,11 +231,11 @@
   \hspace{5mm}$|$ App trm trm\\
   \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm
   & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\
-  \hspace{5mm}$|$ Let \only<2->{as::}assn \only<2->{t::}trm
+  \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm
   & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\
-  \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
   \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\
   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\
@@ -718,11 +738,11 @@
   \hspace{5mm}$|$ App trm trm\\
   \hspace{5mm}$|$ Lam x::name t::trm
   & \isacommand{bind} x \isacommand{in} t\\
-  \hspace{5mm}$|$ Let as::assn t::trm
+  \hspace{5mm}$|$ Let as::assns t::trm
   & \isacommand{bind} bn(as) \isacommand{in} t\\
-  \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
   \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
@@ -745,10 +765,10 @@
   \hspace{5mm}\phantom{$|$} Var name\\
   \hspace{5mm}$|$ App trm trm\\
   \hspace{5mm}$|$ Lam name trm\\
-  \hspace{5mm}$|$ Let assn trm\\
-  \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+  \hspace{5mm}$|$ Let assns trm\\
+  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\[5mm]
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\[5mm]
   \multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
@@ -821,7 +841,7 @@
   \mbox{}\\[6mm]
 
   \begin{center}
-  Let as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\
+  Let as::assns t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\
   \end{center}
 
 
@@ -876,7 +896,7 @@
   \mbox{}\\[6mm]
 
   \begin{center}
-  LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
+  LetRec as::assns t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
   \end{center}
 
 
@@ -1006,22 +1026,22 @@
   \hspace{5mm}$|$ App trm trm\\
   \hspace{5mm}$|$ Lam x::name t::trm
   & \isacommand{bind} x \isacommand{in} t\\
-  \hspace{5mm}$|$ Let as::assn t::trm
+  \hspace{5mm}$|$ Let as::assns t::trm
   & \isacommand{bind} bn(as) \isacommand{in} t\\
-  \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
   \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
   \end{tabular}\bigskip\medskip
 
-  we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
+  we cannot quotient assns: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
 
   \only<1->{
   \begin{textblock}{8}(0.2,7.3)
   \alert{\begin{tabular}{p{2.6cm}}
-  \raggedright\footnotesize{}Should a ``naked'' assn be quotient?
+  \raggedright\footnotesize{}Should a ``naked'' assns be quotient?
   \end{tabular}\hspace{-3mm}
   $\begin{cases}
   \mbox{} \\ \mbox{}