--- a/Quot/Examples/LamEx.thy	Thu Jan 14 15:36:29 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 16:41:17 2010 +0100
@@ -242,11 +242,24 @@
   by (lifting rvar_inject)
 
 lemma lam_induct:
-  "\<lbrakk>\<And>name. P (Var name); 
+  "\<lbrakk>\<And>name. P (Var name);
     \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
     \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
   by (lifting rlam.induct)
 
+lemma lam_induct_strong_pre:
+  "\<lbrakk>\<And>name b. P b (Var name);
+    \<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2);
+    \<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> (c \<bullet> lam)\<rbrakk> \<Longrightarrow> P b (Lam name lam)\<rbrakk> \<Longrightarrow> P a lam"
+sorry
+
+lemma lam_induct_strong:
+  "\<lbrakk>\<And>name. P (Var name);
+    \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+    \<And>name lam. P lam \<Longrightarrow> name \<sharp> lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
+sorry
+
+
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
   apply(simp add: supp_def)