# HG changeset patch
# User huffman
# Date 1200603393 -3600
# Node ID 5fe4b543512e0b697801c1c950772053b5df62b2
# Parent  cb04d05e95fb454d92e61315890fdea0395e3a96
convert lemma lub_mono to rule_format

diff -r cb04d05e95fb -r 5fe4b543512e src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Thu Jan 17 21:44:19 2008 +0100
+++ b/src/HOLCF/Adm.thy	Thu Jan 17 21:56:33 2008 +0100
@@ -77,7 +77,7 @@
     (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
  apply (frule (1) adm_disj_lemma1)
  apply (rule antisym_less)
-  apply (rule lub_mono [rule_format], assumption+)
+  apply (rule lub_mono, assumption+)
   apply (erule chain_mono)
   apply (simp add: adm_disj_lemma2)
  apply (rule lub_range_mono, fast, assumption+)
@@ -128,7 +128,7 @@
 apply (rule lub_mono)
 apply (erule (1) ch2ch_cont)
 apply (erule (1) ch2ch_cont)
-apply assumption
+apply (erule spec)
 done
 
 lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
diff -r cb04d05e95fb -r 5fe4b543512e src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Thu Jan 17 21:44:19 2008 +0100
+++ b/src/HOLCF/Bifinite.thy	Thu Jan 17 21:56:33 2008 +0100
@@ -153,7 +153,7 @@
   fixes x y :: "'a::bifinite_cpo"
   shows "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
-apply (rule lub_mono [rule_format], simp, simp, simp)
+apply (rule lub_mono, simp, simp, simp)
 done
 
 subsection {* Instance for continuous function space *}
diff -r cb04d05e95fb -r 5fe4b543512e src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Thu Jan 17 21:44:19 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Thu Jan 17 21:56:33 2008 +0100
@@ -179,7 +179,7 @@
     \<Longrightarrow> monofun (\<Squnion>i. F i)"
 apply (rule monofunI)
 apply (simp add: thelub_fun)
-apply (rule lub_mono [rule_format])
+apply (rule lub_mono)
 apply (erule ch2ch_fun)
 apply (erule ch2ch_fun)
 apply (simp add: monofunE)
diff -r cb04d05e95fb -r 5fe4b543512e src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jan 17 21:44:19 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jan 17 21:56:33 2008 +0100
@@ -916,7 +916,6 @@
 apply (rule lub_mono)
 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
-apply (rule allI)
 apply (rule prems [unfolded seq.take_def])
 done
 
diff -r cb04d05e95fb -r 5fe4b543512e src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jan 17 21:44:19 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 17 21:56:33 2008 +0100
@@ -73,12 +73,12 @@
 text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
 
 lemma lub_mono:
-  "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<forall>k. X k \<sqsubseteq> Y k\<rbrakk> 
+  "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
 apply (erule is_lub_thelub)
 apply (rule ub_rangeI)
 apply (rule trans_less)
-apply (erule spec)
+apply (erule meta_spec)
 apply (erule is_ub_thelub)
 done
 
@@ -123,7 +123,7 @@
   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
 apply (rule chainI)
-apply (rule lub_mono [rule_format, OF 2 2])
+apply (rule lub_mono [OF 2 2])
 apply (rule chainE [OF 1])
 done
 
@@ -151,7 +151,7 @@
     apply (rule chain_mono [OF 2 le_maxI2])
     done
   show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
-    apply (rule lub_mono [rule_format, OF 3 4])
+    apply (rule lub_mono [OF 3 4])
     apply (rule is_ub_thelub [OF 2])
     done
 qed