diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Tue Jun 14 04:04:09 2005 +0200 +++ b/src/HOLCF/Cont.thy Tue Jun 14 04:05:15 2005 +0200 @@ -235,7 +235,7 @@ apply (blast dest: cont2contlub [THEN contlubE]) done -lemma cont2cont_CF1L_rev2: "(\y. cont (\x. f x y)) \ cont f" +lemma cont2cont_lambda: "(\y. cont (\x. f x y)) \ cont (\x y. f x y)" apply (rule cont2cont_CF1L_rev) apply simp done