--- a/Slides/Slides2.thy	Sun Jul 11 00:58:54 2010 +0100
+++ b/Slides/Slides2.thy	Sun Jul 11 21:18:02 2010 +0100
@@ -44,7 +44,7 @@
   terms involving binders (e.g.~lambda calculus, variable convention)\medskip
   
   \item<2-> \ldots mainly used to find errors in my own 
-  (published) paper proofs and in that of others \alert{\bf ;o)}
+  (published) paper proofs and in those of others \alert{\bf ;o)}
   \end{itemize}
 
   \end{frame}}
@@ -57,7 +57,7 @@
   \begin{frame}<1-3>[c]
   \frametitle{Nominal Theory}
   
-  by Pitts; at its core are:\bigskip
+  \ldots by Pitts; at its core are:\bigskip
 
   \begin{itemize}
   \item sorted atoms and 
@@ -137,6 +137,8 @@
   \item<2-> $\text{[]}\,\act\, x = x$
   \item<2-> $(\pi_1 @  \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$
   \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$
+  \item<2-> if $\pi_1$, $\pi_2$ have dif$\!$f.~type, then
+    $\pi_1 \act (\pi_2 \act x) = \pi_2 \act (\pi_1 \act x)$
   \end{itemize}
   \end{itemize}
 
@@ -161,7 +163,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-5>
+  \begin{frame}<1-4>
   \frametitle{A Better Way}
 *}
 datatype atom = Atom string nat
@@ -169,27 +171,27 @@
 text_raw {*
   \mbox{}\bigskip
   \begin{itemize}
-  \item<3-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
+  \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
 
      \begin{itemize}
      \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)
      \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)
      \end{itemize}\medskip
      
-  \item<4-> \alert{What about {\bf swappings}?}
+  \item<3-> \alert{What about {\bf swappings}?}
      \small
      \[
      \begin{array}{l@ {\hspace{1mm}}l}
      (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
         & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
           \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\
-        & \text{else}\;\only<4>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}
-          \only<5->{\text{\alert{\bf id}}}
+        & \text{else}\;\only<3>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}
+          \only<4->{\text{\alert{\bf id}}}
      \end{array}
      \]
   \end{itemize}
 
-  \only<3>{
+  \only<2>{
   \begin{textblock}{7}(4,11)
   @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   \end{textblock}}
@@ -270,7 +272,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1-2>
-  \frametitle{Solution}
+  \frametitle{Our Solution}
 
 
   \begin{itemize}
@@ -408,12 +410,12 @@
 
   \begin{itemize}
   \item the formalised version of the nominal theory is now much nicer to 
-  work with (sorts are occasionally explicit, \alert{@{text "\<forall>\<pi>. P"}})\medskip
+  work with (sorts are occasionally explicit, \alert{$\forall \pi. P$})\medskip
 
   \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip
 
-  \item crucial insight: allow sort-disrespecting swappings%
-  \onslide<2->{ just define them as the identity}%
+  \item the crucial insight: allow sort-disrespecting swappings%
+  \onslide<2->{ \ldots just define them as the identity}\\%
   \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip
 
   \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}