--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -1,23 +1,10 @@
 theory Ind_General_Scheme 
-imports Simple_Inductive_Package Ind_Prelims
+imports Ind_Interface
 begin
 
-(*<*)
-datatype trm =
-  Var "string"
-| App "trm" "trm"
-| Lam "string" "trm"
+section {* The Code in a Nutshell\label{sec:nutshell} *}
 
-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