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