--- a/Slides/Slides1.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Slides/Slides1.thy	Wed May 26 15:34:54 2010 +0200
@@ -23,7 +23,7 @@
   \large General Bindings\\[15mm]
   \end{tabular}}
   \begin{center}
-  joint work with {\bf Cezary} and Brian Huffman\\[0mm] 
+  joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -33,10 +33,28 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>
+  \begin{frame}<1-2>
   \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
   \mbox{}\\[-3mm]
 
+  \begin{itemize}
+  \item sorted atoms and sort-respecting permutations\medskip
+
+  \onslide<2->{
+  \item[] in old Nominal: atoms have dif\!ferent type
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{7mm}}c}
+  $[] \act c \dn c$ &
+  @{text "(a b)::\<pi> \<bullet> c \<equiv>"} 
+  $\begin{cases}
+  \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\
+  \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\
+  \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}
+  \end{cases}$
+  \end{tabular}
+  \end{center}}
+  \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -45,6 +63,30 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{\begin{tabular}{c}Problems\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$
+
+  \item $supp \_ :: \beta \Rightarrow \alpha set$
+
+  \begin{center}
+  $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$
+  \end{center}
+  
+  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
   \begin{frame}<1>[c]
   \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
   \mbox{}\\[-3mm]