src/HOLCF/Cont.thy

--- a/src/HOLCF/Cont.thy	Mon May 23 19:39:45 2005 +0200
+++ b/src/HOLCF/Cont.thy	Mon May 23 23:01:27 2005 +0200
@@ -384,6 +384,11 @@
 apply (blast dest: cont2contlub [THEN contlubE])
 done
 
+lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1"
+apply (rule cont2cont_CF1L_rev)
+apply simp
+done
+
 text {*
   What D.A.Schmidt calls continuity of abstraction
   never used here