--- a/Nominal/Nominal2_Abs.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Nominal/Nominal2_Abs.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -51,7 +51,7 @@
   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
   and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
   by (case_tac [!] bs, case_tac [!] cs) 
-     (auto simp add: le_fun_def le_bool_def alphas)
+     (auto simp: le_fun_def le_bool_def alphas)
 
 section {* Equivariance *}
 
@@ -87,7 +87,7 @@
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
   unfolding alphas fresh_star_def
   using a
-  by (auto simp add: fresh_minus_perm)
+  by (auto simp: fresh_minus_perm)
 
 lemma alpha_trans:
   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
@@ -204,7 +204,7 @@
   unfolding alphas
   unfolding fresh_star_def
   by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
-     (auto simp add: fresh_minus_perm)
+     (auto simp: fresh_minus_perm)
 
 lemma alphas_abs_trans:
   shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
@@ -278,9 +278,9 @@
     using set_renaming_perm2 by blast
   from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from 0 have 1: "(supp x - as) \<sharp>* p" using *
-    by (auto simp add: fresh_star_def fresh_perm)
+    by (auto simp: fresh_star_def fresh_perm)
   then have 2: "(supp x - as) \<inter> supp p = {}"
-    by (auto simp add: fresh_star_def fresh_def)
+    by (auto simp: fresh_star_def fresh_def)
   have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
   have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))" 
@@ -303,7 +303,7 @@
 lemma alpha_abs_res_minimal:
   assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
   shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
-  using asm unfolding alpha_res by (auto simp add: Diff_Int)
+  using asm unfolding alpha_res by (auto simp: Diff_Int)
 
 lemma alpha_abs_res_abs_set:
   assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
@@ -323,7 +323,7 @@
 lemma alpha_abs_set_abs_res:
   assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
   shows "(as, x) \<approx>res (op =) supp p (as', x')"
-  using asm unfolding alphas by (auto simp add: Diff_Int)
+  using asm unfolding alphas by (auto simp: Diff_Int)
 
 lemma alpha_abs_res_stronger1:
   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
@@ -344,15 +344,15 @@
   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
   then have zb: "p \<bullet> as = p' \<bullet> as" 
-    apply(auto simp add: permute_set_def)
+    apply(auto simp: permute_set_def)
     apply(rule_tac x="xa" in exI)
     apply(simp)
     done
   have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)
   from 0 have 1: "(supp x - as) \<sharp>* p" using *
-    by (auto simp add: fresh_star_def fresh_perm)
+    by (auto simp: fresh_star_def fresh_perm)
   then have 2: "(supp x - as) \<inter> supp p = {}"
-    by (auto simp add: fresh_star_def fresh_def)
+    by (auto simp: fresh_star_def fresh_def)
   have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
   have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as" 
@@ -390,9 +390,9 @@
   then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)
   have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)
   from 0 have 1: "(supp x - set as) \<sharp>* p" using *
-    by (auto simp add: fresh_star_def fresh_perm)
+    by (auto simp: fresh_star_def fresh_perm)
   then have 2: "(supp x - set as) \<inter> supp p = {}"
-    by (auto simp add: fresh_star_def fresh_def)
+    by (auto simp: fresh_star_def fresh_def)
   have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto
   have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast
   also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> 
@@ -420,14 +420,14 @@
   and   "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow> 
    (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs alpha_abs_set_stronger1)[1]
+apply(auto simp: alphas_abs)[1]
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs alpha_abs_res_stronger1)[1]
+apply(auto simp: alphas_abs)[1]
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs alpha_abs_lst_stronger1)[1]
+apply(auto simp: alphas_abs)[1]
 done
 
 lemma alpha_res_alpha_set:
@@ -603,7 +603,7 @@
   unfolding swap_set_not_in[OF a1 a2] 
   using a1 a2
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
+     (auto simp: supp_perm swap_atom)
 
 lemma Abs_swap2:
   assumes a1: "a \<notin> (supp x) - (set bs)"
@@ -616,7 +616,7 @@
   unfolding swap_set_not_in[OF a1 a2]
   using a1 a2
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
+     (auto simp: supp_perm swap_atom)
 
 lemma Abs_supports:
   shows "((supp x) - as) supports ([as]set. x)"
@@ -732,7 +732,7 @@
   and   "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
   and   "as \<sharp>* ([cs]lst. x) \<longleftrightarrow> (as - set cs) \<sharp>* x"
   unfolding fresh_star_def
-  by (auto simp add: Abs_fresh_iff)
+  by (auto simp: Abs_fresh_iff)
 
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
@@ -740,7 +740,7 @@
   and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)"
   and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)"
   unfolding fresh_star_def
-  by(auto simp add: Abs_fresh_iff)
+  by(auto simp: Abs_fresh_iff)
 
 lemma Abs_fresh_star2:
   fixes x::"'a::fs"
@@ -760,7 +760,7 @@
   and   "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
   and   "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
 unfolding Abs_eq_iff2 alphas
-by (auto simp add: supp_perm_singleton fresh_star_def fresh_zero_perm)
+by (auto simp: supp_perm_singleton fresh_star_def fresh_zero_perm)
 
 lemma Abs1_eq_iff_fresh:
   fixes x y::"'a::fs"
@@ -808,28 +808,28 @@
   fixes x y::"'a::fs"
   and z::"'c::fs"
   and a b::"'b::at"
-  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
 apply(auto) 
 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(1))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(2))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(3))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 done
 
 lemma Abs1_eq_iff:
@@ -918,7 +918,7 @@
   shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
   and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
-using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
+using assms by (auto simp: Abs1_eq_iff fresh_permute_left)
 
 
 ML {*
@@ -1078,7 +1078,7 @@
 lemma prod_fv_supp:
   shows "prod_fv supp supp = supp"
 by (rule ext)
-   (auto simp add: supp_Pair)
+   (auto simp: supp_Pair)
 
 lemma prod_alpha_eq:
   shows "prod_alpha (op=) (op=) = (op=)"

--- a/ROOT	Fri Sep 06 10:06:41 2013 +0100
+++ b/ROOT	Sun Oct 13 23:09:21 2013 +0200
@@ -69,4 +69,39 @@
      "~~/src/HOL/Library/LaTeXsugar"
    theories 
      "Paper"
-   files "document/root.bib" "document/root.tex" 
\ No newline at end of file
+   files "document/root.bib" "document/root.tex"
+
+session Slides1 in "Slides" = Nominal2 +
+  options [document = pdf, document_output= "..", document_variants = "slides1"]
+  theories
+    "Slides1"
+
+session Slides2 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides2"]
+  theories
+    "Slides2"
+
+session Slides3 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides3"]
+  theories
+    "Slides3"
+
+session Slides4 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides4"]
+  theories
+    "Slides4"
+
+session Slides5 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides5"]
+  theories
+    "Slides5"
+
+session Slides9 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides9"]
+  theories
+    "Slides9"
+
+session SlidesB in "Slides" = Nominal2 +
+  options [document = pdf, document_output= "..", document_variants = "slidesb"]
+  theories
+    "SlidesB" 
\ No newline at end of file

--- a/Slides/Slides1.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides1.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides1
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)

--- a/Slides/Slides2.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides2.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides2
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)
@@ -385,7 +385,7 @@
 
   {\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]"}\\
+  @{text "sort_ty (\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^sub>1, sort_ty \<tau>\<^sub>2]"}\\
   \end{tabular}}
   \pause
   \isanewline\isanewline

--- a/Slides/Slides3.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides3.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides3
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 declare [[show_question_marks = false]]

--- a/Slides/Slides4.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides4.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides4
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 declare [[show_question_marks = false]]

--- a/Slides/Slides5.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides5.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides5
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)

--- a/Slides/Slides9.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides9.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides9
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/SlidesB.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -0,0 +1,735 @@
+(*<*)
+theory SlidesB
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
+begin
+
+notation (latex output)
+  set ("_") and
+  Cons  ("_::/_" [66,65] 65) 
+
+(*>*)
+
+
+text_raw {*
+  %% was \begin{colormixin}{20!averagebackgroundcolor}
+  %% 
+  %% is \begin{colormixin}{50!averagebackgroundcolor}
+  \renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{%
+  \begin{tabular}{@ {}c@ {}}
+  \Huge Nominal Isabelle\\[0mm]
+  \Large or, How Not to be Intimidated by\\[-3mm]
+  \Large the Variable Convention\\[-5mm]
+  \end{tabular}}
+  
+  \begin{center}
+  Christian Urban\\[1mm]
+  King's College London\\[-6mm]\mbox{}
+  \end{center}
+ 
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \small
+  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\\[2mm]
+  
+  \footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+  \end{block}
+  \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{}
+  \end{itemize}
+  
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \footnotesize
+  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\hfill ---Henk Barendregt
+  \end{block}
+  \end{center}\pause
+
+  \mbox{}\\[-19mm]\mbox{}
+
+  \begin{itemize}
+  \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning 
+  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
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Nominal Techniques}
+
+  \begin{itemize}
+  \item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:
+  \begin{center}
+  \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} 
+  \end{center}
+
+  \item also permutations and substitutions commute, if you suspend permutations
+  in front of variables
+  \begin{center}
+  \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}
+  \end{center}\medskip\medskip
+
+  \item this allowed us to define as simple Nominal Unification algorithm\medskip
+  \begin{center}
+  \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}
+  \smath{\nabla \vdash a \fresh^? t}
+  \end{center}
+  \end{itemize}
+
+  %\begin{textblock}{3}(13.1,1.3)
+  %\includegraphics[scale=0.26]{andrewpitts.jpg}
+  %\end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Nominal Isabelle}
+
+  \begin{itemize}
+  \item a general theory about atoms and permutations\medskip
+  \begin{itemize}
+  \item sorted atoms and
+  \item sort-respecting permutations
+  \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{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 
+  syntax trees
+  %
+  %\item $\alpha$-equivalence
+  %\begin{center}
+  %\begin{tabular}{l}
+  %\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]
+  %\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ 
+  %\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\
+  %\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}
+  %\end{tabular}
+  %\end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-7>
+  \frametitle{New Types in HOL}
+
+   \begin{center}
+  \begin{tikzpicture}[scale=1.5]
+  %%%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \onslide<2-4,6->{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+  \onslide<1-4,6->{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+  \onslide<3-5,6->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+  
+  \onslide<3-4,6->{\draw (-2.0, 0.845) --  (0.7,0.845);}
+  \onslide<3-4,6->{\draw (-2.0,-0.045)  -- (0.7,-0.045);}
+
+  \onslide<4-4,6->{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+  \onslide<4-5,6->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+  \onslide<1-4,6->{\draw (1.8, 0.48) node[right=-0.1mm]
+    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6->{\alert{(sets of raw terms)}}\end{tabular}};}
+  \onslide<2-4,6->{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+  \onslide<3-5,6->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+  
+  \onslide<3-4,6->{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
+  \onslide<3-4,6->{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
+
+  \onslide<6->{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+  \end{tikzpicture}
+  \end{center}
+  
+  \begin{center}
+  \textcolor{red}{\large\bf\onslide<6->{define \boldmath$\alpha$-equivalence}}
+  \end{center}
+
+  \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.};
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>[c]
+  \frametitle{HOL vs.~Nominal}
+
+  \begin{itemize}
+  \item Nominal logic by Pitts are incompatible 
+  with choice principles\medskip
+
+  \item HOL includes Hilbert's epsilon\pause\bigskip
+
+  \item The solution: Do not require that everything has finite support\medskip
+
+  \begin{center}
+  \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x))  \quad\Rightarrow\quad} a \fresh a.x}
+  \end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-5>
+  \frametitle{\begin{tabular}{c}Our Work\end{tabular}}
+  \mbox{}\\[-6mm]
+
+    \begin{center}
+  \begin{tikzpicture}[scale=1.5]
+  %%%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+  \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+  \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+  
+  \onslide<1>{\draw (-2.0, 0.845) --  (0.7,0.845);}
+  \onslide<1>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}
+
+  \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+  \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+  \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]
+    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}
+  \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+  \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+  
+  \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);}
+  \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<4-> derive a {\bf stronger} cases lemma
+  \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\
+  \begin{center}
+  \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} 
+  \end{center}
+  \end{itemize}
+  \end{textblock}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Nominal Isabelle} 
+
+  \begin{itemize}
+  \item Users can 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 _. _")
+
+
+text_raw {*
+  \mbox{}\bigskip
+
+  \begin{itemize}
+  \item These are \underline{\bf named} alpha-equivalence classes, for example
+  \end{itemize}
+
+  \begin{center}
+  \gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{\Large (Weak) Induction Principles} 
+
+  \begin{itemize}
+  \item The usual induction principle for lambda-terms is as follows:
+
+  \begin{center}
+  \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}
+  \centering\smath{%
+  \infer{P\,t}
+  {\begin{array}{l}
+  \forall x.\;P\,x\\[2mm]
+  \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]
+  \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\
+  \end{array}
+  }}
+  \end{beamercolorbox}
+  \end{center}
+
+  \item It requires us in the lambda-case to show the property \smath{P} for
+  all binders \smath{x}.\smallskip\\ 
+
+  (This nearly always requires renamings and they can be 
+  tricky to automate.)
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{\Large Strong Induction Principles} 
+
+  \begin{itemize}
+  \item Therefore we introduced the following strong induction principle:
+
+  \begin{center}
+  \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
+  \centering\smath{%
+  \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%
+         \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%
+         \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}
+  {\begin{array}{l}
+  \forall x\,c.\;P\,c\;x\\[2mm]
+  \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)
+  \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]
+  \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} 
+  \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
+  \end{array}
+  }}
+  \end{beamercolorbox}
+  \end{center}
+  \end{itemize}
+
+  \begin{textblock}{11}(0.9,10.9)
+  \only<2>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)
+  { The variable over which the induction proceeds:\\[2mm]
+    \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};
+
+  \path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);
+  \end{tikzpicture}}
+
+  \only<3>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)
+  {The {\bf context} of the induction; i.e.~what the binder should be fresh for
+   $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]
+   ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} 
+     and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};
+
+  \path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);
+  \end{tikzpicture}}
+
+  \only<4>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)
+  {The property to be proved by induction:\\[-3mm]
+  \begin{center}\small
+  \begin{tabular}{l}
+  \smath{\!\!\lambda
+  (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]
+  \hspace{8mm}
+  \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}  
+  \end{tabular}
+  \end{center}};
+
+  \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item binding sets of names has some interesting properties:\medskip
+  
+  \begin{center}
+  \begin{tabular}{l}
+  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}
+  \bigskip\smallskip\\
+
+  \onslide<2->{%
+  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}
+  }\bigskip\smallskip\\
+
+  \onslide<3->{%
+  \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}
+  }\medskip\\
+  \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}
+  \end{tabular}
+  \end{center}
+  \end{itemize}
+  
+  \begin{textblock}{8}(2,14.5)
+  \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct
+  \end{textblock}
+
+  \only<4>{
+  \begin{textblock}{6}(2.5,4)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\normalsize\color{darkgray}
+  \begin{minipage}{8cm}\raggedright
+  For type-schemes the order of bound names does not matter, and
+  $\alpha$-equivalence is preserved under \alert{vacuous} binders.
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item alpha-equivalence being preserved under vacuous binders is \underline{not} always
+  wanted:\bigskip\bigskip\normalsize
+  
+  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
+  $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\
+  \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}
+   \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}
+    \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}
+  \end{tabular}}
+  
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip
+  
+  \begin{center}
+  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
+  $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\
+  $\;\;\;\not\approx_\alpha
+   \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$
+  \end{tabular}}
+  \end{center}
+  
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<2-3>
+  \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}
+  \mbox{}\\[-6mm]
+
+  \mbox{}\hspace{10mm}
+  \begin{tabular}{ll}
+  \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
+  \hspace{5mm}\phantom{$|$} Var name\\
+  \hspace{5mm}$|$ App trm trm\\
+  \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm
+  & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\
+  \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm
+  & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\
+  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
+  \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
+  \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
+  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}}\\
+  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}}\\
+  \end{tabular}
+
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{So Far So Good}
+
+  \begin{itemize}
+  \item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}
+  \end{itemize}
+
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \small%
+  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\\[2mm]
+  
+  \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+  \end{block}
+  \end{center}
+
+  \mbox{}\\[-18mm]\mbox{}
+
+  \begin{columns}
+  \begin{column}[t]{4.7cm}
+  Inductive Definitions:\\
+  \begin{center}
+  \smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}
+  \end{center}
+  \end{column}
+  \begin{column}[t]{7cm}
+  Rule Inductions:\\[2mm]
+  \begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}
+  1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]
+  2.) & Show the property for\\ & the conclusion.\\
+  \end{tabular}
+  \end{column}
+  \end{columns}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
+  \begin{frame}[sqeeze]
+  \frametitle{Faulty Reasoning} 
+
+  %\mbox{}
+
+  \begin{itemize}
+  \item Consider the two-place relation \smath{\text{foo}}:\medskip
+  \begin{center}
+  \begin{tabular}{ccc}
+  \raisebox{2.5mm}{\colorbox{cream}{%
+  \smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}
+  &
+  \raisebox{2mm}{\colorbox{cream}{%
+  \smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}
+  &
+  \colorbox{cream}{%
+  \smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]
+  \end{tabular}
+  \end{center}
+
+  \pause
+
+  \item The lemma we going to prove:\smallskip
+  \begin{center}
+  Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.
+  \end{center}\bigskip
+
+  \only<3>{
+  \item Cases 1 and 2 are trivial:\medskip
+  \begin{itemize}
+  \item If \smath{y\fresh x} then \smath{y\fresh x}.
+  \item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.
+  \end{itemize}
+  }
+
+  \only<4->{
+  \item Case 3:
+  \begin{itemize}
+  \item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.}; 
+  We have to show \smath{y\fresh t'}.$\!\!\!\!$ 
+  \item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.
+  \item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!
+  \end{itemize}
+  }
+  \end{itemize}
+  
+  \begin{textblock}{11.3}(0.7,0.6)
+  \only<5-7>{
+  \begin{tikzpicture}
+  \draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)
+  {{\bf Variable Convention:}\\[2mm] 
+  \small
+   If $M_1,\ldots,M_n$ occur in a certain mathematical context
+   (e.g. definition, proof), then in these terms all bound variables 
+   are chosen to be different from the free variables.\smallskip
+
+  \normalsize
+   {\bf In our case:}\\[2mm]
+   The free variables are \smath{y} and \smath{t'}; the bound one is 
+   \smath{x}.\medskip
+          
+   By the variable convention we conclude that \smath{x\not= y}.
+  };
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \begin{textblock}{9.2}(3.6,9)
+  \only<6,7>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)
+  {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow
+          y\!\not\in\! \text{fv}(t)\!-\!\{x\}
+          \stackrel{x\not=y}{\Longleftrightarrow}
+          y\!\not\in\! \text{fv}(t)}};
+
+  \path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Conclusions} 
+
+  \begin{itemize}
+  \item The user does not see anything of the ``raw'' level.
+  \item The Nominal Isabelle automatically derives the strong structural
+  induction principle for \underline{\bf all} nominal datatypes (not just the 
+  lambda-calculus)
+
+  \item They are easy to use: you just have to think carefully what the variable
+  convention should be.
+
+  \item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners 
+  of the variable convention: when and where it can be used safely.
+  
+  \item<2> \alert{\bf Main Point:} Actually these proofs using the
+  variable convention are all trivial / obvious / routine\ldots {\bf provided} 
+  you use Nominal Isabelle. ;o)
+ 
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[b]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[13mm]
+  \alert{\LARGE Thank you very much!}\\
+  \alert{\Large Questions?}
+  \end{tabular}}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/beamerthemeplaincu.sty	Sun Oct 13 23:09:21 2013 +0200
@@ -0,0 +1,118 @@
+%%\Providespackage{beamerthemeplainculight}[2003/11/07 ver 0.93]
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+
+% Copyright 2003 by Till Tantau <tantau@cs.tu-berlin.de>.
+%
+% This program can be redistributed and/or modified under the terms
+% of the LaTeX Project Public License Distributed from CTAN
+% archives in directory macros/latex/base/lppl.txt.
+ 
+\newcommand{\slidecaption}{}
+
+\mode<presentation>
+
+\usepackage{fontspec}
+\usefonttheme{serif}
+\defaultfontfeatures{Ligatures=TeX}
+\setromanfont{Hoefler Text}
+\setmonofont[Scale=MatchLowercase]{Consolas}
+\newfontfamily{\consolas}{Consolas}
+\newcommand{\tttext}[1]{{\consolas{#1}}}
+%%\setttfont{Lucida Console}
+%%\setmainfont[Mapping=tex-text]{Hoefler Text}
+
+%%\renewcommand\ttdefault{lmtt}
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% comic fonts fonts
+%\DeclareFontFamily{T1}{comic}{}%
+%\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
+%\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
+%\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
+%\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
+%\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
+%\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
+%\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
+%\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
+%
+%\renewcommand{\rmdefault}{comic}%
+%\renewcommand{\sfdefault}{comic}%
+\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one
+%
+\DeclareMathVersion{bold}% mathfont needs to be bold
+\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}%
+\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}%
+\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}%
+\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}%
+\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}%
+\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}%
+\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frametitles
+
+\setbeamerfont{frametitle}{size={\LARGE}}
+\setbeamerfont{frametitle}{family={\fontspec{Hoefler Text Black}}}
+%\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}
+\setbeamercolor{frametitle}{fg=ProcessBlue,bg=white}
+
+\setbeamertemplate{frametitle}{%
+\vskip 2mm  % distance from the top margin
+\hskip -3mm % distance from left margin
+\vbox{%
+\begin{minipage}{1.05\textwidth}%
+\centering%
+\insertframetitle%
+\end{minipage}}%
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Foot
+%
+\setbeamertemplate{navigation symbols}{} 
+\usefoottemplate{%
+\vbox{%
+  \tinyline{%
+    \tiny\hfill\textcolor{gray!50}{\slidecaption{} --
+      p.~\insertframenumber/\inserttotalframenumber}}}%
+}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\beamertemplateballitem
+\setlength\leftmargini{2mm}
+\setlength\leftmarginii{0.6cm}
+\setlength\leftmarginiii{1.5cm}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% blocks
+%\definecolor{cream}{rgb}{1,1,.65}
+\definecolor{cream}{rgb}{1,1,.8}
+\setbeamerfont{block title}{size=\normalsize}
+\setbeamercolor{block title}{fg=black,bg=cream}
+\setbeamercolor{block body}{fg=black,bg=cream}
+
+\setbeamertemplate{blocks}[rounded][shadow=true]
+
+\setbeamercolor{boxcolor}{fg=black,bg=cream}
+
+\mode
+<all>
+
+
+
+
+
+

--- a/Slides/document/root.tex	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/document/root.tex	Sun Oct 13 23:09:21 2013 +0200
@@ -1,9 +1,9 @@
-\usepackage{beamerthemeplainculight}
-
-\usepackage[T1]{fontenc}
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{beamerthemeplaincu}
+%%%\usepackage[T1]{fontenc}
 \usepackage{proof}
 \usepackage{german}
-\usepackage[latin1]{inputenc}
+%%%\usepackage[latin1]{inputenc}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{mathpartir}
@@ -31,7 +31,7 @@
 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
 \newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
 \renewcommand{\emptyset}{\varnothing}% nice round empty set
-\renewcommand{\Gamma}{\varGamma} 
+%%\renewcommand{\Gamma}{\varGamma} 
 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
 \newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}

Binary file slides1.pdf has changed

Binary file slides2.pdf has changed

Binary file slides3.pdf has changed

Binary file slides4.pdf has changed

Binary file slides5.pdf has changed

Binary file slides9.pdf has changed

Binary file slidesb.pdf has changed