--- a/Slides/Slides3.thy	Sun Jul 11 00:58:54 2010 +0100
+++ b/Slides/Slides3.thy	Sun Jul 11 21:18:02 2010 +0100
@@ -9,24 +9,54 @@
 
 (*>*)
 
+text_raw {*
+  \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Quiz}
+  
+  Assuming that \smath{a} and \smath{b} are distinct variables,\\
+  is it possible to find $\lambda$-terms \smath{M_1} to \smath{M_7} 
+  that make the following pairs \alert{$\alpha$-equivalent}?
+
+  \begin{tabular}{@ {\hspace{14mm}}p{12cm}}
+  \begin{itemize}
+  \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_1)\;}
+
+  \item \smath{\lambda a.\lambda b. (M_2\,b)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_3)\;}
+
+  \item \smath{\lambda a.\lambda b. (b\,M_4)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_5)\;}
+
+  \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 
+        \smath{\lambda a.\lambda a. (a\,M_7)\;}
+  \end{itemize}
+  \end{tabular}
+
+  If there is one solution for a pair, can you describe all its solutions?
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
 text_raw {*
-  \renewcommand{\slidecaption}{Cambridge, 8.~June 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/HOL\\[5mm]
+  \huge Nominal Unification\\[-2mm] 
+  \Large Hitting a Sweet Spot\\[5mm]
   \end{tabular}}
   \begin{center}
   Christian Urban
   \end{center}
   \begin{center}
-  joint work with {\bf Cezary Kaliszyk}\\[0mm] 
+  \small initial work with Andy Pitts and Jamie Gabbay\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%