--- 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)"
--- 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 *}
--- 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)
--- 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
--- 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