# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263488240 -3600
# Node ID cd3f1409780ad8ebbd87359cdd5f10a9f1740fbe
# Parent  f2a1ebba9bdc9c950d9369103001c1bab54b5b96
right generalisation

diff -r f2a1ebba9bdc -r cd3f1409780a Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Thu Jan 14 17:53:23 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 17:57:20 2010 +0100
@@ -263,7 +263,7 @@
   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)" 
+  have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" 
   proof (induct lam rule: lam_induct)
     case (1 name pi)
     show "P a (pi \<bullet> Var name)"
@@ -272,13 +272,14 @@
       done
   next
     case (2 lam1 lam2 pi)
-    have b1: "P a (pi \<bullet> lam1)" by fact
-    have b2: "P a (pi \<bullet> lam2)" by fact
+    have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact
+    have b2: "\<And>(pi::name prm) a. 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
+      apply (rule b1)
+      apply (rule b2)
+      done
   next
     case (3 name lam pi)
     have b: "P a (pi \<bullet> lam)" by fact