diff -r 842969a598f2 -r f961a32eb0d9 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Sat Jul 10 11:27:04 2010 +0100
+++ b/Slides/Slides2.thy	Sat Jul 10 15:50:33 2010 +0100
@@ -11,19 +11,20 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
+  \renewcommand{\slidecaption}{Edinburgh, 11.~July 2010}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1>[t]
   \frametitle{%
   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
   \\
-  \huge Nominal 2\\[-2mm] 
-  \large Or, How to Reason Conveniently with\\[-5mm]
-  \large General Bindings in Isabelle\\[15mm]
+  \LARGE Proof Pearl:\\[-2mm]
+  \LARGE A New Foundation for\\[-2mm] 
+  \LARGE Nominal Isabelle\\[12mm]
   \end{tabular}}
   \begin{center}
-  joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 
+  \small
+  Brian Huf\!fman and {\bf Christian Urban}\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -34,7 +35,37 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1-2>
-  \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
+  \frametitle{\begin{tabular}{c}Nominal Isabelle\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item sorted atoms and sort-respecting permutations\medskip
+
+  \onslide<2->{
+  \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{7mm}}c}
+  $[]\;\act\;c \dn c$ &
+  $(a\;b)\!::\!\pi\;\act\;c \dn$ 
+  $\begin{cases}
+  b & \text{if}\; \pi \act c = a\\
+  a & \text{if}\; \pi \act c = b\\
+  \pi \act c & \text{otherwise}
+  \end{cases}$
+  \end{tabular}
+  \end{center}}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-2>
+  \frametitle{\begin{tabular}{c}Nominal Theory\end{tabular}}
   \mbox{}\\[-3mm]
 
   \begin{itemize}