# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233248996 0
# Node ID 667a0943c40bc059635c0af9bd06afd7a9e13723
# Parent  b071a0b88298cdd758dd0abaf2d074e44dd8beaa
added a section that will eventually describe the code

diff -r b071a0b88298 -r 667a0943c40b CookBook/Package/Ind_Code.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/Ind_Code.thy	Thu Jan 29 17:09:56 2009 +0000
@@ -0,0 +1,22 @@
+theory Ind_Code
+imports "../Base" Simple_Inductive_Package
+begin
+
+text {*
+
+  @{ML_chunk [display,gray] induction_rules}
+
+*}
+
+text {*
+
+  @{ML_chunk [display,gray] intro_rules}
+
+*}
+
+text {*
+
+  @{ML_chunk [display,gray] storing}
+
+*}
+end
diff -r b071a0b88298 -r 667a0943c40b CookBook/Package/Ind_Intro.thy
--- a/CookBook/Package/Ind_Intro.thy	Thu Jan 29 17:08:39 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Thu Jan 29 17:09:56 2009 +0000
@@ -15,20 +15,20 @@
   \end{flushright}
 
   \medskip
-  Higher order logic, as implemented in Isabelle/HOL, is based on just a few
-  primitive constants, like equality, implication, and the description
-  operator, whose properties are described as axioms. All other concepts, such
-  as inductive predicates, datatypes, or recursive functions are defined in
-  terms of those constants, and the desired properties, for example induction
-  theorems, or recursion equations are derived from the definitions by a
-  formal proof. Since it would be very tedious for a user to define complex
-  inductive predicates or datatypes ``by hand'' just using the primitive
-  operators of higher order logic, Isabelle/HOL already contains a number of
-  packages automating such work. Thanks to those packages, the user can give a
-  high-level specification, like a list of introduction rules or constructors,
-  and the package then does all the low-level definitions and proofs behind
-  the scenes. In this chapter we explain how such a package can be
-  implemented.
+  HOL is based on just a few primitive constants, like equality, implication,
+  and the description operator, whose properties are described as axioms. All
+  other concepts, such as inductive predicates, datatypes, or recursive
+  functions are defined in terms of those constants, and the desired
+  properties, for example induction theorems, or recursion equations are
+  derived from the definitions by a formal proof. Since it would be very
+  tedious for a user to define complex inductive predicates or datatypes ``by
+  hand'' just using the primitive operators of higher order logic,
+  Isabelle/HOL already contains a number of packages automating such
+  work. Thanks to those packages, the user can give a high-level
+  specification, like a list of introduction rules or constructors, and the
+  package then does all the low-level definitions and proofs behind the
+  scenes. In this chapter we explain how such a package can be implemented.
+
 
   %The packages are written in Standard ML, the implementation
   %language of Isabelle, and can be invoked by the user from within theory documents
diff -r b071a0b88298 -r 667a0943c40b CookBook/Package/simple_inductive_package.ML
--- a/CookBook/Package/simple_inductive_package.ML	Thu Jan 29 17:08:39 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Thu Jan 29 17:09:56 2009 +0000
@@ -42,10 +42,10 @@
        end) (preds_syn ~~ preds ~~ Tss) lthy;
 
     val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
-
-
+ 
+     
     (* proving the induction rules *)
-
+    (* @chunk induction_rules *)
     val (Pnames, lthy3) =
       Variable.variant_fixes (replicate (length preds) "P") lthy2;
     val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT))
@@ -76,10 +76,10 @@
       end;
 
     val indrules = map prove_indrule (preds ~~ Ps ~~ Tss);
-
+    (* @end *)
 
     (* proving the introduction rules *)
-
+    (* @chunk intro_rules *) 
     val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
     val imp_elims = fold (fn th => fn th' => [th', th] MRS mp);
 
@@ -112,12 +112,13 @@
       singleton (ProofContext.export lthy2 lthy1);
 
     val intr_ths = map_index prove_intr intrs;
-
+    (* @end *)
 
     (* storing the theorems *)
-
+    (* @chunk storing *)
     val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn);
     val case_names = map (Binding.base_name o fst o fst) intrs
+    (* @end *)
   in
     lthy1 |>
     LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
@@ -133,7 +134,7 @@
           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
          (preds_syn ~~ indrules)) #>> maps snd)
   end;
-
+   
 (* @chunk add_inductive *)
 fun add_inductive preds_syn params_syn intro_srcs lthy =
   let