diff -r a21fb87bb0bd -r 447b433b67fa Slides/Slides2.thy
--- a/Slides/Slides2.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/Slides/Slides2.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -49,20 +49,20 @@
   Oc ("1") and
   Bk ("0") and
   exponent ("_\<^bsup>_\<^esup>" [107] 109) and
-  inv_begin0 ("I\<^isub>0") and
-  inv_begin1 ("I\<^isub>1") and
-  inv_begin2 ("I\<^isub>2") and
-  inv_begin3 ("I\<^isub>3") and
-  inv_begin4 ("I\<^isub>4") and 
+  inv_begin0 ("I\<^sub>0") and
+  inv_begin1 ("I\<^sub>1") and
+  inv_begin2 ("I\<^sub>2") and
+  inv_begin3 ("I\<^sub>3") and
+  inv_begin4 ("I\<^sub>4") and 
   inv_begin ("I\<^bsub>cbegin\<^esub>") and
-  inv_loop1 ("J\<^isub>1") and
-  inv_loop0 ("J\<^isub>0") and
-  inv_end1 ("K\<^isub>1") and
-  inv_end0 ("K\<^isub>0") and
-  recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
-  Pr ("Pr\<^isup>_") and
-  Cn ("Cn\<^isup>_") and
-  Mn ("Mn\<^isup>_") and
+  inv_loop1 ("J\<^sub>1") and
+  inv_loop0 ("J\<^sub>0") and
+  inv_end1 ("K\<^sub>1") and
+  inv_end0 ("K\<^sub>0") and
+  recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
+  Pr ("Pr\<^sup>_") and
+  Cn ("Cn\<^sup>_") and
+  Mn ("Mn\<^sup>_") and
   tcopy ("copy") and 
   tcontra ("contra") and
   tape_of ("\<langle>_\<rangle>") and 
@@ -563,10 +563,10 @@
 
 (*<*)
 lemmas HR1 = 
-  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]
 
 lemmas HR2 =
-  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
 (*>*)
 
 text_raw {*
@@ -615,18 +615,18 @@
   \begin{center}\small
   \begin{tabular}{@ {}l@ {}}
   \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
-  @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-  @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
-  @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+  @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+  @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
   \end{tabular}\bigskip\bigskip
   \\
   \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
   $\inferrule*{
-    \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
-    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
-    \\ @{term "{P\<^isub>3} dither \<up>"}
+    \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
+    {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
+    \\ @{term "{P\<^sub>3} dither \<up>"}
    }
-   {@{term "{P\<^isub>1} tcontra \<up>"}}
+   {@{term "{P\<^sub>1} tcontra \<up>"}}
   $
   \end{tabular}
   \end{tabular}
@@ -640,18 +640,18 @@
   \begin{center}\small
   \begin{tabular}{@ {}l@ {}}
   \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}
-  @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-  @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
-  @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+  @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+  @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
   \end{tabular}\bigskip\bigskip
   \\
   \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
   $\inferrule*{
-    \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
-    {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
-    \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
+    \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
+    {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
+    \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}
    }
-   {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
+   {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
   $
   \end{tabular}
   \end{tabular}
@@ -818,8 +818,8 @@
 
   \small
   \begin{tabular}{l}
-  @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^isub>0, e), (W\<^isub>1, exit); Label exit"}\\
-  \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^isub>0, e), (W\<^isub>1, e)"}
+  @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^sub>0, e), (W\<^sub>1, exit); Label exit"}\\
+  \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^sub>0, e), (W\<^sub>1, e)"}
   \end{tabular}
 
   \end{frame}}
@@ -913,7 +913,7 @@
   \item we introduced some tactics for handling sequential programs\bigskip
 
   \begin{center}
-  @{text "\<lbrace>p\<rbrace> i:[c\<^isub>1 ; ... ; c\<^isub>n]:j \<lbrace>q\<rbrace>"}
+  @{text "\<lbrace>p\<rbrace> i:[c\<^sub>1 ; ... ; c\<^sub>n]:j \<lbrace>q\<rbrace>"}
   \end{center}\bigskip\bigskip
 
   \item for loops we often only have to do inductions on the length