# HG changeset patch
# User huffman
# Date 1116882087 -7200
# Node ID 603820cad0835b48773a77ca0760209722a397fc
# Parent  880b0e786c1b04f98598137f9d1a3cd472af5a4a
moved theorem cont2cont_CF1L_rev2 to Cont.thy

diff -r 880b0e786c1b -r 603820cad083 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