# HG changeset patch
# User huffman
# Date 1117834489 -7200
# Node ID 7ff978ca1920a864f2aececdea2feb92e2f9cf0d
# Parent  e3816a7db01627dec352b97956fd43c3e261aadf
changed to use new contlubI, etc.

diff -r e3816a7db016 -r 7ff978ca1920 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Fri Jun 03 23:33:48 2005 +0200
+++ b/src/HOLCF/Up.thy	Fri Jun 03 23:34:49 2005 +0200
@@ -157,10 +157,10 @@
 subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
 
 lemma monofun_Iup: "monofun(Iup)"
-by (simp add: monofun)
+by (simp add: monofun_def)
 
 lemma monofun_Ifup1: "monofun(Ifup)"
-apply (rule monofunI [rule_format])
+apply (rule monofunI)
 apply (rule less_fun [THEN iffD2, rule_format])
 apply (rule_tac p = "xa" in upE)
 apply simp
@@ -169,7 +169,7 @@
 done
 
 lemma monofun_Ifup2: "monofun(Ifup(f))"
-apply (rule monofunI [rule_format])
+apply (rule monofunI)
 apply (rule_tac p = "x" in upE)
 apply simp
 apply simp
@@ -376,7 +376,7 @@
 text {* continuity for @{term Iup} *}
 
 lemma cont_Iup [iff]: "cont(Iup)"
-apply (rule contI [rule_format])
+apply (rule contI)
 apply (rule is_lub_Iup)
 apply (erule thelubE [OF _ refl])
 done
@@ -386,7 +386,7 @@
 text {* continuity for @{term Ifup} *}
 
 lemma contlub_Ifup1: "contlub(Ifup)"
-apply (rule contlubI [rule_format])
+apply (rule contlubI)
 apply (rule trans)
 apply (rule_tac [2] thelub_fun [symmetric])
 apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
@@ -399,7 +399,7 @@
 done
 
 lemma contlub_Ifup2: "contlub(Ifup(f))"
-apply (rule contlubI [rule_format])
+apply (rule contlubI)
 apply (case_tac "EX i x. Y i = Iup x")
 apply (erule exE)
 apply (subst thelub_up1c)