Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use thelub_const lemma
authorhuffman
Fri, 27 May 2005 00:16:18 +0200
changeset 16093 cdcbf5a7f38d
parent 16092 a1a481ee9425
child 16094 a92ee2833938
use thelub_const lemma
src/HOLCF/Cfun.thy file | annotate | diff | comparison | revisions
src/HOLCF/Cprod.thy file | annotate | diff | comparison | revisions 
--- 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)
--- 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))"
isabelle