--- a/src/HOLCF/FOCUS/Fstreams.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstreams.thy Mon Mar 22 20:54:52 2010 -0700
@@ -324,15 +324,6 @@
lemma cpo_cont_lemma:
"[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f"
-apply (rule monocontlub2cont, auto)
-apply (simp add: contlub_def, auto)
-apply (erule_tac x="Y" in allE, auto)
-apply (simp add: po_eq_conv)
-apply (frule cpo,auto)
-apply (frule is_lubD1)
-apply (frule ub2ub_monofun, auto)
-apply (drule thelubI, auto)
-apply (rule is_lub_thelub, auto)
-by (erule ch2ch_monofun, simp)
+by (erule contI2, simp)
end