diff -r 0634d42bb69f -r 17b1512f51af ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 24 18:06:20 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Mar 25 15:09:04 2009 +0100
@@ -83,7 +83,7 @@
 val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] 
 val eo_prednames = [@{binding "even"}, @{binding "odd"}]
 val eo_syns = [NoSyn, NoSyn] 
-val eo_arg_tyss = [[@{typ "nat"}],[@{typ "nat"}]] *}
+val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] *}
 
 
 ML{*val fresh_defs = [@{thm fresh_def}]
@@ -103,7 +103,7 @@
 subsection {* Definitions *}
 
 text {*
-  First we have to produce for each predicate the definition, whose general form is
+  We first have to produce for each predicate the definition, whose general form is
 
   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
@@ -124,7 +124,7 @@
 text {*
   It returns the definition (as a theorem) and the local theory in which this definition has 
   been made. In Line 4, @{ML internalK in Thm} is a flag attached to the 
-  theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). 
+  theorem (others possibilities are the flags @{ML definitionK in Thm} and @{ML axiomK in Thm}). 
   These flags just classify theorems and have no significant meaning, except 
   for tools that, for example, find theorems in the theorem database. We also
   use @{ML empty_binding in Attrib} in Line 3, since the definition does 
@@ -133,7 +133,7 @@
 
 local_setup %gray {* fn lthy =>
 let
-  val arg =  ((@{binding "MyTrue"}, NoSyn), @{term True})
+  val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})
   val (def, lthy') = make_defs arg lthy 
 in
   warning (str_of_thm_no_vars lthy' def); lthy'
@@ -218,7 +218,8 @@
   The second function for the definitions has to just iterate the function
   @{ML defs_aux} over all predicates. The argument @{text "preds"} is again
   the the list of predicates as @{ML_type term}s; the argument @{text
-  "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is
+  "prednames"} is the list of names of the predicates; @{text syns} are the
+  syntax annotations for each predicate; @{text "arg_tyss"} is
   the list of argument-type-lists for each predicate.
 *}
 
@@ -283,10 +284,10 @@
 *}
 
 lemma manual_ind_prin: 
-assumes prem: "even n"
-shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+assumes prem: "even z"
+shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
 apply(atomize (full))
-apply(cut_tac prems)
+apply(cut_tac prem)
 apply(unfold even_def)
 apply(drule spec[where x=P])
 apply(drule spec[where x=Q])
@@ -370,6 +371,13 @@
 done
 
 text {*
+  This gives the theorem:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{thm [source] automatic_ind_prin}\\
+  @{text "> "}~@{thm automatic_ind_prin}
+  \end{isabelle}
+
   While the tactic for the induction principle is relatively simple, 
   it is a bit harder to construct the goals from the introduction 
   rules the user provides. In general we have to construct for each predicate 
@@ -417,7 +425,7 @@
   The variables are applied to the predicate in Line 7 (this corresponds
   to the first premise @{text "pred zs"} of the induction principle). 
   In Line 8 and 9, we first construct the term  @{text "P zs"} 
-  and then add the (substituded) introduction rules as premises. In case that
+  and then add the (substituted) introduction rules as premises. In case that
   no introduction rules are given, the conclusion of this implication needs
   to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
   mechanism will fail. 
@@ -428,7 +436,7 @@
   which the introduction rules have been substituted. The code in these two
   lines will return a theorem. However, it is a theorem
   proved inside the local theory @{text "lthy'"}, where the variables @{text
-  "zs"} are fixed, but free. By exporting this theorem from @{text
+  "zs"} are fixed, but free (see Line 4). By exporting this theorem from @{text
   "lthy'"} (which contains the @{text "zs"} as free) to @{text
   "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.
   A testcase for this function is
@@ -457,7 +465,7 @@
 
   Note that the export from @{text lthy'} to @{text lthy} in Line 13 above 
   has turned the free, but fixed, @{text "z"} into a schematic 
-  variable @{text "?z"}. The @{text "P"} and @{text "Q"} are not yet
+  variable @{text "?z"}; the variables @{text "P"} and @{text "Q"} are not yet
   schematic. 
 
   We still have to produce the new predicates with which the introduction
@@ -515,8 +523,8 @@
 @{text [display]
 "> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> 
 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
-> odd ?z \<Longrightarrow> ?P1 0 
-> \<Longrightarrow> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
+> odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
+> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
 
   Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic
   variables. The numbers have been introduced by the pretty-printer and are 
@@ -575,41 +583,31 @@
 "warning (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
-*}
 
-ML {* prems_of *}
-ML {* Logic.strip_params *}
-ML {* Logic.strip_assums_hyp *}
+  We now look closely at the proof for the introduction rule
 
-ML {*
-fun chop_print (params1, params2) (prems1, prems2) ctxt =
-let
-  val _ = warning ((commas params1) ^ " | " ^ (commas params2))
-  val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^
-                   (commas (map (Syntax.string_of_term ctxt) prems2)))
-in
-   ()
-end
+  \begin{isabelle}
+  @{term "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"}
+  \end{isabelle}
+  
 *}
 
 
-
-lemma intro1:
-  shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
-apply(tactic {* ObjectLogic.rulify_tac 1 *})
-apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
-apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
-oops
-
-ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
-
-
 lemma fresh_App:
-  shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+  shows "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
 apply(tactic {* ObjectLogic.rulify_tac 1 *})
 apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
 apply(tactic {* print_tac "" *})
+
+txt {*
+  \begin{isabelle}
+  @{subgoals}
+  \end{isabelle}
+*}
+
+ML_prf {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
+
 apply(tactic {* SUBPROOF_test (fn {params, prems, ...} =>
    let
      val (prems1, prems2) = chop (length prems - length fresh_rules) prems