--- a/CookBook/Package/Ind_Code.thy	Thu Mar 12 15:43:22 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Thu Mar 12 18:39:10 2009 +0000
@@ -24,7 +24,7 @@
   been made. What is @{ML Thm.internalK}?
 *}
 
-ML {*let
+ML{*let
   val lthy = TheoryTarget.init NONE @{theory}
 in
   make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
@@ -70,6 +70,18 @@
   the (fresh) arguments of the predicate.
 *}
 
+ML{*let
+  val orules = [@{term "even 0"},
+                @{term "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
+                @{term "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] 
+  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+in
+  warning
+    (Syntax.string_of_term @{context} 
+      (defs_aux @{context} orules preds (@{term "even::nat\<Rightarrow>bool"}, [@{typ "nat"}])))
+end*}
+
+
 text {*
   The arguments of the main function for the definitions are 
   the intro rules; the predicates and their names, their syntax 
@@ -94,7 +106,6 @@
   The actual definitions are made in Line 7.  
 *}
 
-
 subsection {* Induction Principles *}
 
 ML{*fun inst_spec ct = 
@@ -172,6 +183,7 @@
   val cnewpreds = map (cterm_of thy) newpreds
   val rules' = map (subst_free (preds ~~ newpreds)) rules
 
+
   fun prove_induction ((pred, newpred), tys)  =
   let
     val zs = replicate (length tys) "z"
@@ -184,18 +196,17 @@
   in
     Goal.prove lthy3 [] [prem] goal
       (fn {prems, ...} => induction_tac defs prems cnewpreds)
-      |> singleton (ProofContext.export lthy3 lthy1)
+       |> singleton (ProofContext.export lthy3 lthy1)
   end 
 in
   map prove_induction (preds ~~ newpreds ~~ tyss)
 end*}
 
-(*
 ML {*
   let 
-    val rules = [@{term "even 0"},
-                 @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
-                 @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
+    val rules = [@{prop "even (0::nat)"},
+                 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+                 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
     val defs = [@{thm even_def}, @{thm odd_def}]
     val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
     val tyss = [[@{typ "nat"}],[@{typ "nat"}]]
@@ -203,7 +214,6 @@
     inductions rules defs preds tyss @{context}
   end
 *}
-*)
 
 subsection {* Introduction Rules *}
 
@@ -242,6 +252,21 @@
           REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
           subproof1 rules preds i ctxt]*}
 
+lemma evenS: 
+  shows "odd m \<Longrightarrow> even (Suc m)"
+apply(tactic {* 
+let
+  val rules = [@{prop "even (0::nat)"},
+                 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+                 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
+  val defs = [@{thm even_def}, @{thm odd_def}]
+  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+in
+  introductions_tac defs rules preds 1 @{context}
+end *})
+done
+
+
 ML{*fun introductions rules preds defs lthy = 
 let
   fun prove_intro (i, goal) =