diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Package/Simple_Inductive_Package.thy
--- a/CookBook/Package/Simple_Inductive_Package.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-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