Quot/Examples/LamEx.thy
changeset 890 0f920b62fb7b
parent 889 cff21786d952
child 891 7bac7dffadeb
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 11:04:21 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 12:17:30 2010 +0100
@@ -377,6 +377,9 @@
     (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and>
     (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
   )"
-apply (lifting hom)
+(*apply (lifting hom)*)
+sorry
+
+thm rlam.recs
 
 end