diff -r cf451e182bf0 -r b7b80d5640bb Slides/SlidesB.thy
--- a/Slides/SlidesB.thy	Sun Oct 13 23:09:21 2013 +0200
+++ b/Slides/SlidesB.thy	Mon Oct 14 11:23:18 2013 +0200
@@ -27,7 +27,7 @@
   
   \begin{center}
   Christian Urban\\[1mm]
-  King's College London\\[-6mm]\mbox{}
+  King's College London\\[-4mm]\mbox{}
   \end{center}
  
   \begin{center}
@@ -54,8 +54,27 @@
   \begin{frame}<1->[c]
   \frametitle{}
 
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-2mm}}c@ {}}
+  \includegraphics[scale=0.36]{phd-2.jpg}\,
+  \includegraphics[scale=0.36]{phd-1.jpg}\\
+  \hfill\textcolor{gray}{\small dinner after my PhD examination}
+  \end{tabular}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{}
+
   \begin{itemize}
-  \item \normalsize Aim: develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
+  \item \normalsize Aim: develop Nominal Isabelle for reasoning formally about 
+  programming languages\\[-10mm]\mbox{}
   \end{itemize}
   
   \begin{center}
@@ -76,7 +95,7 @@
   about LF (and fixed it in three ways)
   \item found also fixable errors in my Ph.D.-thesis about cut-elimination
   (examined by Henk Barendregt and Andy Pitts)
-  \item found the variable convention can in principle be used for proving false
+  \item found that the variable convention can in principle be used for proving false
   \end{itemize}
 
   \end{frame}}
@@ -127,18 +146,18 @@
   \item a general theory about atoms and permutations\medskip
   \begin{itemize}
   \item sorted atoms and
-  \item sort-respecting permutations
+  \item sort-respecting permutations\bigskip
   \end{itemize}
   
   \item support and freshness
   \begin{center}
   \begin{tabular}{l}
-  \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\
+  \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\[2mm]
   \smath{a \fresh x \dn a \notin \textit{supp}(x)}
   \end{tabular}
   \end{center}\bigskip\pause
 
-  \item allow users to reason about alpha-equivalence classes like about 
+  \item allow users to reason about alpha-equivalence classes as if they were 
   syntax trees
   %
   %\item $\alpha$-equivalence
@@ -194,8 +213,8 @@
   \begin{textblock}{9}(2.8,12.5)
   \only<7>{
   \begin{tikzpicture}
-  \draw (0,0) node[fill=cream, text width=8cm, thick, draw=red, rounded corners=1mm] (nn)
-  {The ``new types'' are the reason why there is no Nominal Coq.};
+  \draw (0,0) node[fill=cream, text width=8.5cm, thick, draw=red, rounded corners=1mm] (nn)
+  {The ``new types mechanism'' is the reason why there is no Nominal Coq.};
   \end{tikzpicture}}
   \end{textblock}
 
@@ -210,10 +229,10 @@
   \frametitle{HOL vs.~Nominal}
 
   \begin{itemize}
-  \item Nominal logic by Pitts are incompatible 
+  \item Nominal logic by Pitts is incompatible 
   with choice principles\medskip
 
-  \item HOL includes Hilbert's epsilon\pause\bigskip
+  \item but HOL includes Hilbert's epsilon\pause\bigskip
 
   \item The solution: Do not require that everything has finite support\medskip
 
@@ -254,15 +273,15 @@
   \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
   \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
 
-  \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+  %%\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
   \end{tikzpicture}
   \end{center}
   
   \begin{textblock}{9.5}(6,3.5)
   \begin{itemize}
-  \item<1-> defined fv and $\alpha$
-  \item<2-> built quotient / new type
-  \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) 
+  \item<1-> define fv and $\alpha$
+  \item<2-> build quotient / new type
+  \item<3-> derive a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) 
   \item<4-> derive a {\bf stronger} cases lemma
   \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\
   \begin{center}
@@ -284,15 +303,15 @@
   \frametitle{Nominal Isabelle} 
 
   \begin{itemize}
-  \item Users can define lambda-terms as:
+  \item Users can for example define lambda-terms as:
   \end{itemize}
 *}
       
  atom_decl name   text_raw {*\medskip\isanewline *}
 	nominal_datatype lam =
-	    Var "name"
-	  | App "lam" "lam" 
-	  | Lam x::"name" t::"lam" binds x in t ("Lam _. _")
+	    Var name
+	  | App lam lam 
+	  | Lam x::name t::lam   binds x in t ("Lam _. _")
 
 
 text_raw {*
@@ -335,7 +354,7 @@
   \end{center}
 
   \item It requires us in the lambda-case to show the property \smath{P} for
-  all binders \smath{x}.\smallskip\\ 
+  all binders \smath{x}.\medskip\\ 
 
   (This nearly always requires renamings and they can be 
   tricky to automate.)
@@ -664,7 +683,7 @@
   \end{tikzpicture}}
   \end{textblock}
 
-  \begin{textblock}{9.2}(3.6,9)
+  \begin{textblock}{9.2}(3.6,9.2)
   \only<6,7>{
   \begin{tikzpicture}[remember picture]
   \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)