diff -r ac064c47138b -r e2be455093a1 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Sat Jul 10 23:36:45 2010 +0100
+++ b/Slides/Slides2.thy	Sun Jul 11 00:58:54 2010 +0100
@@ -100,7 +100,7 @@
 
   \only<3>{
   \begin{textblock}{14}(1,12.5)
-  \alert{The big benefit:} the type system takes care of the sort-respecting part.
+  \alert{The big benefit:} the type system takes care of the sort-respecting requirement.
   \end{textblock}}
   \only<4>{
   \begin{textblock}{14}(1,12.5)
@@ -148,7 +148,7 @@
   \begin{itemize}
   \item \alert{lots} of ML-code 
   \item \alert{not} pretty 
-  \item \alert{not a proof pearl} :o( 
+  \item \alert{not a {\bf proof pearl}} :o( 
   \end{itemize}
   \end{quote}};
   \end{tikzpicture}
@@ -176,7 +176,7 @@
      \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)
      \end{itemize}\medskip
      
-  \item<4-> \alert{What about swappings?}
+  \item<4-> \alert{What about {\bf swappings}?}
      \small
      \[
      \begin{array}{l@ {\hspace{1mm}}l}
@@ -191,7 +191,7 @@
 
   \only<3>{
   \begin{textblock}{7}(4,11)
-  @{text "\<pi> \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+  @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   \end{textblock}}
   
   \end{frame}}
@@ -219,7 +219,8 @@
    \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$
    \end{itemize}\medskip
 
-   \onslide<7->{\alert{$\;\mapsto\;$}only one type class, $\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
+   \onslide<7->{\alert{$\;\mapsto\;$}only one type class needed, $\text{finite}(\text{supp}\;x)$,\\
+   \hspace{9mm}$\forall \pi. P$}
   \end{itemize}
 
   \only<5>{
@@ -241,8 +242,35 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-3>
+  \begin{frame}<1>[c]
   \frametitle{One Snatch}
+*}
+
+datatype \<iota>atom = \<iota>Atom string nat
+
+
+text_raw {*
+  \isanewline\isanewline
+  \begin{itemize}
+  \item You like to get the advantages of the old way back: you 
+  \alert{cannot mix} atoms of dif$\!$ferent sort:\bigskip
+  
+  \small
+  e.g.~LF-objects:
+  \begin{center}
+  $\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$
+  \end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-2>
+  \frametitle{Solution}
 
 
   \begin{itemize}
@@ -259,30 +287,19 @@
 text_raw {*
   \mbox{}\bigskip\bigskip
   \begin{itemize}
-  \item<2-> there is an overloaded  function \alert{\bf atom}, which injects concrete 
+  \item they are a ``subtype'' of the generic atom type
+  \item there is an overloaded  function \alert{\bf atom}, which injects concrete 
   atoms into generic ones\medskip 
   \begin{center}
   \begin{tabular}{l}
   $\text{atom}(a) \fresh x$\\
   $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$
   \end{tabular}
-  \end{center}\bigskip\medskip
-
-  \onslide<3->
-  {One would like to have $a \fresh x$, $(a\; b)$, \ldots}
+  \end{center}
+  \pause
+  One would like to have $a \fresh x$, $\swap{a}{b}$, \ldots
   \end{itemize}
 
-  \only<1>{
-  \begin{textblock}{11}(2.5,8.5)
-  You like to get the advantages of the old way back: you \alert{cannot mix} atoms
-  of dif$\!$ferent sort:\bigskip
-  
-  \small
-  e.g.~LF-objects:\\[-9mm]\mbox{} 
-  \begin{center}$\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$
-  \end{center}
-  \end{textblock}}
-
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -317,7 +334,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-3>
+  \begin{frame}<1-2>
   \frametitle{Non-Working Solution}
 
 Instead of\isanewline\isanewline
@@ -330,7 +347,7 @@
 \isanewline\isanewline
 *}
 
-    datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+    datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota> 'a nat
 text_raw {*
   \pause
   \isanewline\isanewline
@@ -342,30 +359,42 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+(*<*)
+hide_const sort
+(*>*)
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-3>
+  \begin{frame}<1-4>
   \frametitle{A Working Solution}
 
 *}
     datatype sort = Sort string "sort list"
-    datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-
-text_raw {*
-\isanewline\isanewline
-have
-\isanewline\isanewline
-*}
-
-    datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+    datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
+(*<*)
+consts sort_ty :: "nat \<Rightarrow> sort"
+(*>*)
 text_raw {*
   \pause
+  \isanewline
+
+  {\small\begin{tabular}{rcl}
+  @{text "sort_ty (TVar x)"}  & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\
+  @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}\\
+  \end{tabular}}
+  \pause
   \isanewline\isanewline
-  But then
-  \begin{center}
-  @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-  \end{center}
+  \isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"}
+  \pause
+  \isanewline\isanewline
+  \small
+  \begin{minipage}{12cm}
+  @{text "Var x \<tau> \<equiv> \<lceil> Atom (sort_ty \<tau>) x \<rceil>"}\isanewline
+
+  @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau> = Var y \<tau>"}\\
+  @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau>' = Var x \<tau>'"}\\
+  \end{minipage}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -373,17 +402,22 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-2>[c]
+  \begin{frame}<1-4>[c]
   \frametitle{Conclusion}
   \mbox{}\\[-3mm]
 
   \begin{itemize}
   \item the formalised version of the nominal theory is now much nicer to 
-  work with (sorts are occasionally explicit)\bigskip
+  work with (sorts are occasionally explicit, \alert{@{text "\<forall>\<pi>. P"}})\medskip
+
+  \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip
 
-  \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip
+  \item crucial insight: allow sort-disrespecting swappings%
+  \onslide<2->{ just define them as the identity}%
+  \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip
 
-  \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}
+  \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}
+  in Austin Texas
   \end{itemize}
 
   
@@ -391,6 +425,21 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[23mm]
+  \alert{\LARGE Thank you very much}\\
+  \alert{\Large Questions?}
+  \end{tabular}}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file