# HG changeset patch
# User huffman
# Date 1117834692 -7200
# Node ID af5ed1a10cd7f333f9bf29d3f6cca380c4c1acc9
# Parent  ea49a9c7ff7c5106de47d86dbf109e9d26dc017e
fixed renamed theorems

diff -r ea49a9c7ff7c -r af5ed1a10cd7 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)