--- a/CookBook/Package/Simple_Inductive_Package.thy	Sun Mar 08 20:53:00 2009 +0000
+++ b/CookBook/Package/Simple_Inductive_Package.thy	Tue Mar 10 13:20:46 2009 +0000
@@ -1,8 +1,62 @@
 theory Simple_Inductive_Package
-imports Main
-uses ("simple_inductive_package.ML")
+imports Main "../Base"
+uses "simple_inductive_package.ML"
 begin
 
+(*
+simple_inductive
+  trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl R x x"
+| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
+
+thm trcl_def
+thm trcl.induct
+thm trcl.intros
+
+simple_inductive
+  even and odd
+where
+  even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
+
+thm even_def odd_def
+thm even.induct odd.induct
+thm even0
+thm evenS
+thm oddS
+thm even_odd.intros
+
+simple_inductive
+  accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  accpartI: "(\<forall>y. r y x \<longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
+
+thm accpart_def
+thm accpart.induct
+thm accpartI
+
+locale rel =
+  fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+simple_inductive (in rel) accpart'
+where
+  accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
+
+
+context rel
+begin
+  thm accpartI'
+  thm accpart'.induct
+end
+
+thm rel.accpartI'
+thm rel.accpart'.induct
+
+
+lemma "True" by simp
+*)
 
 use_chunks "simple_inductive_package.ML"