--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -1,5 +1,5 @@
 theory Ind_Code
-imports "../Base" "../FirstSteps" Ind_General_Scheme 
+imports "../Base" "../FirstSteps" Ind_Interface Ind_General_Scheme
 begin
 
 section {* The Gory Details\label{sec:code} *} 
@@ -798,7 +798,7 @@
 *}
 
 lemma accpartI:
-  shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+  shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})
 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})
 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
@@ -879,7 +879,7 @@
 *}
 
 lemma accpartI:
-  shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+  shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply(tactic {* expand_tac @{thms accpart_def} *})
 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})
 done
@@ -1058,7 +1058,7 @@
 
 ML{*val specification =
   spec_parser >>
-    (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
+    (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
 
 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 
               "define inductive predicates"
@@ -1083,6 +1083,7 @@
   
 *}
 
+(*
 simple_inductive
   Even and Odd
 where
@@ -1100,19 +1101,25 @@
 
 thm Even_def
 thm Odd_def
+*)
 
+(*
 text {* 
   Second, we want that the user can specify fixed parameters.
   Remember in the previous section we stated that the user can give the 
   specification for the transitive closure of a relation @{text R} as 
 *}
+*)
 
+(*
 simple_inductive
   trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
   base: "trcl\<iota>\<iota> R x x"
 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
+*)
 
+(*
 text {*
   Note that there is no locale given in this specification---the parameter
   @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
@@ -1132,14 +1139,15 @@
   But this does not correspond to the induction principle we derived by hand, which
   was
   
-  \begin{center}\small
-  \mprset{flushleft}
-  \mbox{\inferrule{
-             @{thm_style prem1  trcl_induct[no_vars]}\\\\
-             @{thm_style prem2  trcl_induct[no_vars]}\\\\
-             @{thm_style prem3  trcl_induct[no_vars]}}
-            {@{thm_style concl  trcl_induct[no_vars]}}}  
-  \end{center}
+  
+  %\begin{center}\small
+  %\mprset{flushleft}
+  %\mbox{\inferrule{
+  %           @ { thm_style prem1  trcl_induct[no_vars]}\\\\
+  %           @ { thm_style prem2  trcl_induct[no_vars]}\\\\
+  %           @ { thm_style prem3  trcl_induct[no_vars]}}
+  %          {@ { thm_style concl  trcl_induct[no_vars]}}}  
+  %\end{center}
 
   The difference is that in the one derived by hand the relation @{term R} is not
   a parameter of the proposition @{term P} to be proved and it is also not universally
@@ -1151,7 +1159,7 @@
   to write 
 
 *}
-
+*)
 (*
 simple_inductive
   trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -1164,5 +1172,4 @@
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
 *)
-
-end
+(*<*)end(*>*)
\ No newline at end of file