# HG changeset patch
# User huffman
# Date 1117145778 -7200
# Node ID cdcbf5a7f38df350f06e43e196dae991db482adf
# Parent  a1a481ee9425e6e07f88e7a4499fbd17abf8bf14
use thelub_const lemma

diff -r a1a481ee9425 -r cdcbf5a7f38d src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri May 27 00:15:24 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Fri May 27 00:16:18 2005 +0200
@@ -632,7 +632,7 @@
 apply (rule contlubI [rule_format])
 apply (case_tac "x = \<bottom>")
 apply (simp add: Istrictify1)
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
 apply (simp add: Istrictify2)
 apply (erule contlub_cfun_fun)
 done
@@ -641,7 +641,7 @@
 apply (rule contlubI [rule_format])
 apply (case_tac "lub (range Y) = \<bottom>")
 apply (simp add: Istrictify1 chain_UU_I)
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
 apply (simp add: Istrictify2)
 apply (simp add: contlub_cfun_arg)
 apply (rule lub_equal2)
diff -r a1a481ee9425 -r cdcbf5a7f38d src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Fri May 27 00:15:24 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Fri May 27 00:16:18 2005 +0200
@@ -138,14 +138,14 @@
 apply (rule contlubI [rule_format])
 apply (subst thelub_cprod)
 apply (erule monofun_pair1 [THEN ch2ch_monofun])
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
 done
 
 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
 apply (rule contlubI [rule_format])
 apply (subst thelub_cprod)
 apply (erule monofun_pair2 [THEN ch2ch_monofun])
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
 done
 
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"