diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Package/Ind_General_Scheme.thy
--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Sat Aug 31 08:07:45 2013 +0100
@@ -41,11 +41,11 @@
 
 text {*
   The inductive package will generate the reasoning infrastructure for
-  mutually recursive predicates, say @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+  mutually recursive predicates, say @{text "pred\<^sub>1\<dots>pred\<^sub>n"}. In what
   follows we will have the convention that various, possibly empty collections
   of ``things'' (lists, terms, nested implications and so on) are indicated either by
   adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes]
-  "\<^isup>*"}. The shorthand for the predicates will therefore be @{text
+  "\<^sup>*"}. The shorthand for the predicates will therefore be @{text
   "preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must
   be, of course, at least a single one in order to obtain a meaningful
   definition.
@@ -58,7 +58,7 @@
   \begin{isabelle}
   @{text "rule ::= 
   \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> 
-  \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$> 
+  \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^raw:}}_{\text{\rm recursive premises}}$> 
   \<Longrightarrow> pred ts"}
   \end{isabelle}
   
@@ -68,7 +68,7 @@
   @{text Bs} in a @{text "rule"} stand for formulae not involving the
   inductive predicates @{text "preds"}; the instances @{text "pred ss"} and
   @{text "pred ts"} can stand for different predicates, like @{text
-  "pred\<^isub>1 ss"} and @{text "pred\<^isub>2 ts"}, in case mutual recursive
+  "pred\<^sub>1 ss"} and @{text "pred\<^sub>2 ts"}, in case mutual recursive
   predicates are defined; the terms @{text ss} and @{text ts} are the
   arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred
   ts"} is a premise of the rule. The outermost quantified variables @{text
@@ -96,7 +96,7 @@
   replaced by their object logic equivalents. Therefore an @{text "orule"} is
   of the form
 
-  @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
+  @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^sup>* \<longrightarrow> pred ts"}
 
   A definition for the predicate @{text "pred"} has then the form
 
@@ -133,13 +133,13 @@
   also be derived from the @{text defs}. These derivations are a bit involved. 
   Assuming we want to prove the introduction rule 
 
-  @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+  @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
 
   then we have assumptions of the form
 
   \begin{isabelle}
   (i)~~@{text "As"}\\
-  (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
+  (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}
   \end{isabelle}
 
   and must show the goal
@@ -150,7 +150,7 @@
 
   \begin{isabelle}
   (i)~~~@{text "As"}\\
-  (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\
+  (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}\\
   (iii)~@{text "orules"}
   \end{isabelle}
 
@@ -164,14 +164,14 @@
   proving. After transforming the object connectives into meta-connectives, this introduction 
   rule must necessarily be of the form 
 
-  @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+  @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
 
   When we apply this rule we end up in the goal state where we have to prove
   goals of the form
 
   \begin{isabelle}
   (a)~@{text "As"}\\
-  (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
+  (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}
   \end{isabelle}
 
   We can immediately discharge the goals @{text "As"} using the assumptions in 
@@ -180,7 +180,7 @@
   @{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us the 
   assumptions
 
-  @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}
+  @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}
 
   Instantiating the universal quantifiers and then resolving with the assumptions 
   in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.