| 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