diff -r 61d30863e5d1 -r a9e63abf3feb Slides/Slides1.thy
--- a/Slides/Slides1.thy	Wed Mar 02 00:06:28 2011 +0000
+++ b/Slides/Slides1.thy	Tue Mar 08 09:07:27 2011 +0000
@@ -11,7 +11,8 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
+  %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
+  \renewcommand{\slidecaption}{Uppsala, 3.~March 2011}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1>[t]
@@ -187,8 +188,8 @@
 
   \onslide<2->{
   \begin{center}
-  \isacommand{bind\_res}\hspace{6mm}
-  \isacommand{bind\_set}\hspace{6mm}
+  \isacommand{bind (set+)}\hspace{6mm}
+  \isacommand{bind (set)}\hspace{6mm}
   \isacommand{bind}
   \end{center}}
 
@@ -268,19 +269,19 @@
   \begin{center}
   \begin{tabular}{l}
   \isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\
-  \isacommand{bind\_set} a b c \ldots \isacommand{in} x y z \ldots\\
-  \isacommand{bind\_res} a b c \ldots \isacommand{in} x y z \ldots
+  \isacommand{bind (set)} a b c \ldots \isacommand{in} x y z \ldots\\
+  \isacommand{bind (set+)} a b c \ldots \isacommand{in} x y z \ldots
   \end{tabular}
   \end{center}\bigskip\medskip
   the reason is that with our definition of $\alpha$-equivalence\medskip
   \begin{center}
   \begin{tabular}{l}
-  \isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\ 
-  \hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y
+  \isacommand{bind (set+)} as \isacommand{in} x y $\not\Leftrightarrow$\\ 
+  \hspace{8mm}\isacommand{bind (set+)} as \isacommand{in} x, \isacommand{bind (set+)} as \isacommand{in} y
   \end{tabular}
   \end{center}\medskip
 
-  same with \isacommand{bind\_set}
+  same with \isacommand{bind (set)}
   \end{itemize}}
   \end{itemize}
 
@@ -374,7 +375,7 @@
   \begin{tabular}{@ {\hspace{1cm}}l}
   $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}%
            \only<7>{${}_{\text{\alert{list}}}$}%
-           \only<8>{${}_{\text{\alert{res}}}$}}%
+           \only<8>{${}_{\text{\alert{set+}}}$}}%
            \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$
   \end{tabular}\bigskip
   \end{itemize}
@@ -438,7 +439,7 @@
   {\tiny\color{darkgray}
   \begin{minipage}{3.4cm}\raggedright
   \begin{tabular}{r@ {\hspace{1mm}}l}
-  \multicolumn{2}{@ {}l}{res:}\\
+  \multicolumn{2}{@ {}l}{set+:}\\
   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
   $\wedge$ & $\pi \cdot x = y$\\
@@ -497,7 +498,7 @@
   \end{center}
 
   \begin{itemize}
-  \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% 
+  \item $\approx_{\text{set+}}$, $\approx_{\text{set}}$% 
   \only<2>{, \alert{$\not\approx_{\text{list}}$}}
   \end{itemize}
 
@@ -509,7 +510,7 @@
   {\tiny\color{darkgray}
   \begin{minipage}{3.4cm}\raggedright
   \begin{tabular}{r@ {\hspace{1mm}}l}
-  \multicolumn{2}{@ {}l}{res:}\\
+  \multicolumn{2}{@ {}l}{set+:}\\
   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
   $\wedge$ & $\pi \cdot x = y$\\
@@ -567,7 +568,7 @@
   \end{center}
 
   \begin{itemize}
-  \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$,
+  \item $\approx_{\text{set+}}$, $\not\approx_{\text{set}}$,
         $\not\approx_{\text{list}}$
   \end{itemize}
 
@@ -579,7 +580,7 @@
   {\tiny\color{darkgray}
   \begin{minipage}{3.4cm}\raggedright
   \begin{tabular}{r@ {\hspace{1mm}}l}
-  \multicolumn{2}{@ {}l}{res:}\\
+  \multicolumn{2}{@ {}l}{set+:}\\
   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\
   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\
   $\wedge$ & $\pi \cdot x = y$\\
@@ -668,7 +669,7 @@
 
   \only<1->{
   \begin{textblock}{8}(12,3.8)
-  \footnotesize $^*$ set, res, list
+  \footnotesize $^*$ set, set+, list
   \end{textblock}}
   
   \end{frame}}
@@ -883,7 +884,7 @@
   \infer[\text{LetRec-}\!\approx_\alpha]
   {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'}
   {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
-    ^{R,fv} (\text{bn}(as'), (t', as'))} 
+    ^{R,\text{fv}} (\text{bn}(as'), (t', as'))} 
   \]\bigskip
   
   \onslide<1->{\alert{deep recursive binders}}
@@ -933,7 +934,7 @@
 
 
   \item the properties for support are implied by the properties of $[\_].\_$
-  \item we can derive strong induction principles (almost automatic---matter of time)
+  \item we can derive strong induction principles
   \end{itemize}
 
 
@@ -981,7 +982,7 @@
   \begin{itemize}
   \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions
   \begin{center}
-  $\sim$ 1 min
+  $\sim$ 2 mins
   \end{center}
   \end{itemize}
 
@@ -1059,6 +1060,22 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1->[c]
+  \frametitle{\begin{tabular}{c}Future Work\end{tabular}}
+  \mbox{}\\[-6mm]
+
+  \begin{itemize}
+  \item Function definitions 
+  \end{itemize}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
   \frametitle{\begin{tabular}{c}Questions?\end{tabular}}
   \mbox{}\\[-6mm]
 
@@ -1070,6 +1087,8 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -1088,10 +1107,10 @@
   \end{center}
   
   \onslide<2->
-  {1.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$, 
-   \isacommand{bind\_set} as \isacommand{in} $\tau_2$\medskip
+  {1.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$, 
+   \isacommand{bind (set)} as \isacommand{in} $\tau_2$\medskip
 
-   2.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$ $\tau_2$ 
+   2.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$ $\tau_2$ 
   }
 
   \end{frame}}