diff -r cff21786d952 -r 0f920b62fb7b Quot/Examples/LamEx.thy --- 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 @@ (\l r. hom (App l r) = f_app l r (hom l) (hom r)) \ (\x a. hom (Lam a x) = f_lam (\b. ([(a,b)] \ x)) (\b. hom ([(a,b)] \ x))) )" -apply (lifting hom) +(*apply (lifting hom)*) +sorry + +thm rlam.recs end