--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,61 @@
+theory Simple_Inductive_Package
+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: "(\<And>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
+*)
+
+use_chunks "simple_inductive_package.ML"
+
+
+end