diff -r a21fb87bb0bd -r 447b433b67fa Slides/Slides1.thy
--- a/Slides/Slides1.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/Slides/Slides1.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -15,16 +15,16 @@
   Oc ("0") and
   Bk ("1") and
   exponent ("_\<^bsup>_\<^esup>") 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")
+  inv_loop1 ("J\<^sub>1") and
+  inv_loop0 ("J\<^sub>0") and
+  inv_end1 ("K\<^sub>1") and
+  inv_end0 ("K\<^sub>0")