diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Essential.thy	Sat Aug 31 08:07:45 2013 +0100
@@ -699,9 +699,9 @@
 
   \begin{exercise}\label{fun:revsum}
   Write a function @{text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
-  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
-  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
+  term of the form @{text "t\<^sub>1 + t\<^sub>2 + \<dots> + t\<^sub>n"} (whereby @{text "n"} might be one)
+  and returns the reversed sum @{text "t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1"}. Assume
+  the @{text "t\<^sub>i"} can be arbitrary expressions and also note that @{text "+"} 
   associates to the left. Try your function on some examples. 
   \end{exercise}
 
@@ -1514,8 +1514,8 @@
 *}
 
   lemma 
-    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
-    and     assm\<^isub>2: "P t"
+    assumes assm\<^sub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
+    and     assm\<^sub>2: "P t"
     shows "Q t"(*<*)oops(*>*) 
 
 text {*