src/HOLCF/Cont.thy
changeset 16388 1ff571813848
parent 16204 5dd79d3f0105
child 16564 6fc73c9dd5f4
--- 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: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
+lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x y. f x y)"
 apply (rule cont2cont_CF1L_rev)
 apply simp
 done