diff -r 09a64cb04851 -r c3662f845129 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Thu Jan 14 16:41:17 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 17:13:11 2010 +0100
@@ -244,20 +244,42 @@
 lemma lam_induct:
   "\<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"
+    \<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"
+instance lam::pt_name
+apply(default)
+sorry
+
+instance lam::fs_name
+apply(default)
 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
+  fixes a::"'a::fs_name"
+  shows 
+   "\<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> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)\<rbrakk> 
+    \<Longrightarrow> P a lam"
+proof -
+  have "\<And>(pi::name prm). P a (pi \<bullet> lam)" 
+  proof (induct lam rule: lam_induct)
+    case (1 name pi)
+    show "P a (pi \<bullet> Var name)" 
+      apply - 
+      sorry
+  next
+    case (2 lam1 lam2 pi)
+    show "P a (pi \<bullet> App lam1 lam2)" sorry
+  next
+    case (3 name lam pi)
+    show "P a (pi \<bullet> Lam name lam)" sorry
+  qed
+  then have "P a (([]::name prm) \<bullet> lam)" by blast
+  then show "P a lam" by simp 
+qed
 
 
 lemma var_supp: