fixed renamed theorems
authorhuffman
Fri, 03 Jun 2005 23:38:12 +0200
changeset 16219 af5ed1a10cd7
parent 16218 ea49a9c7ff7c
child 16220 fd980649c4b2
fixed renamed theorems
src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Fri Jun 03 23:37:21 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Fri Jun 03 23:38:12 2005 +0200
@@ -340,7 +340,7 @@
 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, 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)