diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Tactical.thy	Sat Aug 31 08:07:45 2013 +0100
@@ -243,9 +243,9 @@
   this consider the proof in Figure~\ref{fig:goalstates}: as can be seen,
   internally every goal state is an implication of the form
 
-  @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
-
-  where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
+  @{text[display] "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}
+
+  where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are
   the subgoals. So after setting up the lemma, the goal state is always of the
   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
   "#C"}. Since the goal @{term C} can potentially be an implication, there is a
@@ -253,7 +253,7 @@
   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
   as a @{text #}). This wrapper prevents that premises of @{text C} are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
-  (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
+  (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic
   variables. This instantiations of schematic variables can be observed 
   on the user level. Have a look at the following definition and proof.
@@ -866,8 +866,8 @@
 sorry
 
 text {* 
-  and you want to apply it to the goal @{term "(t\<^isub>1 t\<^isub>2) \<le>
-  (s\<^isub>1 s\<^isub>2)"}. Since in the theorem all variables are
+  and you want to apply it to the goal @{term "(t\<^sub>1 t\<^sub>2) \<le>
+  (s\<^sub>1 s\<^sub>2)"}. Since in the theorem all variables are
   schematic, we have a nasty higher-order unification problem and @{text rtac}
   will not be able to apply this rule in the way we want. For the goal at hand 
   we want to use it so that @{term R} is instantiated to the constant @{text \<le>} and
@@ -899,7 +899,7 @@
 *}
 
 lemma
-  shows "\<And>t\<^isub>1 s\<^isub>1 (t\<^isub>2::'a) (s\<^isub>2::'a). (t\<^isub>1 t\<^isub>2) \<le> (s\<^isub>1 s\<^isub>2)"
+  shows "\<And>t\<^sub>1 s\<^sub>1 (t\<^sub>2::'a) (s\<^sub>2::'a). (t\<^sub>1 t\<^sub>2) \<le> (s\<^sub>1 s\<^sub>2)"
 apply(tactic {* fo_rtac @{thm rule} @{context} 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
@@ -1377,8 +1377,8 @@
 
   \begin{isabelle}
   \begin{center}
-  \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
-                  {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
+  \mbox{\inferrule{@{text "t\<^sub>1 \<equiv> s\<^sub>1 \<dots> t\<^sub>n \<equiv> s\<^sub>n"}}
+                  {@{text "constr t\<^sub>1\<dots>t\<^sub>n \<equiv> constr s\<^sub>1\<dots>s\<^sub>n"}}}
   \end{center}
   \end{isabelle}
 
@@ -1621,9 +1621,9 @@
 end
 
 lemma perm_append[simp]:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
-by (induct pi\<^isub>1) (auto) 
+  fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+  shows "((pi\<^sub>1@pi\<^sub>2)\<bullet>c) = (pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c))"
+by (induct pi\<^sub>1) (auto) 
 
 lemma perm_bij[simp]:
   fixes c d::"nat" and pi::"prm"
@@ -1636,9 +1636,9 @@
 by (induct pi arbitrary: c) (auto)
 
 lemma perm_compose:
-fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
-by (induct pi\<^isub>2) (auto)
+fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>(pi\<^sub>1\<bullet>c)" 
+by (induct pi\<^sub>2) (auto)
 text_raw {*
 \end{isabelle}
 \end{boxedminipage}
@@ -1666,8 +1666,8 @@
 *}
 
 lemma 
-fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+  shows "pi\<^sub>1\<bullet>(c, pi\<^sub>2\<bullet>((rev pi\<^sub>1)\<bullet>d)) = (pi\<^sub>1\<bullet>c, (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>d)"
 apply(simp)
 apply(rule trans)
 apply(rule perm_compose)
@@ -1689,13 +1689,13 @@
 text {* Now the two lemmas *}
 
 lemma perm_aux_expand:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
+  fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+  shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = pi\<^sub>1 \<bullet>aux (pi\<^sub>2\<bullet>c)" 
 unfolding perm_aux_def by (rule refl)
 
 lemma perm_compose_aux:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
+  fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+  shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>aux c) = (pi\<^sub>1\<bullet>pi\<^sub>2) \<bullet>aux (pi\<^sub>1\<bullet>c)" 
 unfolding perm_aux_def by (rule perm_compose)
 
 text {* 
@@ -1734,8 +1734,8 @@
 *}
 
 lemma 
-  fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+  fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+  shows "pi\<^sub>1\<bullet>(c, pi\<^sub>2\<bullet>((rev pi\<^sub>1)\<bullet>d)) = (pi\<^sub>1\<bullet>c, (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>d)"
 apply(tactic {* perm_simp_tac @{context} 1 *})
 done
 
@@ -2049,7 +2049,7 @@
   into a number. To solve this problem have a look at the next exercise. 
 
   \begin{exercise}\label{ex:addsimproc}
-  Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their 
+  Write a simproc that replaces terms of the form @{term "t\<^sub>1 + t\<^sub>2"} by their 
   result. You can assume the terms are ``proper'' numbers, that is of the form
   @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
   \end{exercise}