--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Tue May 05 03:21:49 2009 +0200
@@ -1,11 +1,44 @@
 theory Ind_General_Scheme 
-imports Ind_Interface
+imports  "../Base" Simple_Inductive_Package
 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"
+
+simple_inductive
+  even and odd
+where
+  even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
+
+simple_inductive
+  accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+
+datatype trm =
+  Var "string"
+| App "trm" "trm"
+| Lam "string" "trm"
+
+simple_inductive 
+  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" 
+where
+  fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
+| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
+| fresh_lam1: "fresh a (Lam a t)"
+| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+(*>*)
+
+
 section {* The Code in a Nutshell\label{sec:nutshell} *}
 
 
-
 text {*
   The inductive package will generate the reasoning infrastructure for
   mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what