equal
deleted
inserted
replaced
287 apply (rule flatdom_strict2cont) |
287 apply (rule flatdom_strict2cont) |
288 apply simp |
288 apply simp |
289 done |
289 done |
290 |
290 |
291 text {* |
291 text {* |
292 \medskip Extension of cont_tac and installation of simplifier. |
292 \medskip Extension of @{text cont_tac} and installation of simplifier. |
293 *} |
293 *} |
294 |
294 |
295 lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1" |
295 lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1" |
296 apply (rule cont2cont_CF1L_rev) |
296 apply (rule cont2cont_CF1L_rev) |
297 apply simp |
297 apply simp |