author | huffman |
Mon, 23 May 2005 23:01:27 +0200 | |
changeset 16053 | 603820cad083 |
parent 16052 | 880b0e786c1b |
child 16054 | b8ba6727712f |
--- 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