--- a/Quot/Examples/LamEx.thy	Thu Jan 14 17:13:11 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 17:53:23 2010 +0100
@@ -258,24 +258,34 @@
 
 lemma lam_induct_strong:
   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"
+  assumes a1: "\<And>name b. P b (Var name)"
+  and     a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
+  and     a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
+  shows "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
+    show "P a (pi \<bullet> Var name)"
+      apply (simp only: pi_var1)
+      apply (rule a1)
+      done
   next
     case (2 lam1 lam2 pi)
-    show "P a (pi \<bullet> App lam1 lam2)" sorry
+    have b1: "P a (pi \<bullet> lam1)" by fact
+    have b2: "P a (pi \<bullet> lam2)" by fact
+    show "P a (pi \<bullet> App lam1 lam2)"
+      apply (simp only: pi_app)
+      apply (rule a2)
+      using b1 b2
+      sorry
   next
     case (3 name lam pi)
-    show "P a (pi \<bullet> Lam name lam)" sorry
+    have b: "P a (pi \<bullet> lam)" by fact
+    show "P a (pi \<bullet> Lam name lam)" 
+      apply (simp add: pi_lam)
+      using b
+      sorry
   qed
   then have "P a (([]::name prm) \<bullet> lam)" by blast
   then show "P a lam" by simp