--- a/src/HOLCF/Adm.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Adm.thy Fri Jan 18 20:22:07 2008 +0100
@@ -21,7 +21,7 @@
"(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
unfolding adm_def by fast
-lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
+lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
unfolding adm_def by fast
lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
@@ -50,7 +50,7 @@
by (rule admI, simp)
lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
-by (fast elim: admD intro: admI)
+by (fast intro: admI elim: admD)
lemma adm_all: "(\<And>y. adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
by (fast intro: admI elim: admD)
@@ -139,7 +139,7 @@
apply (simp add: cont2contlubE)
apply (erule admD)
apply (erule (1) ch2ch_cont)
-apply assumption
+apply (erule spec)
done
lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
--- a/src/HOLCF/CompactBasis.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy Fri Jan 18 20:22:07 2008 +0100
@@ -340,7 +340,7 @@
shows "P x"
apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
apply (simp add: lub_basis_fun_take)
- apply (rule admD [rule_format, OF adm])
+ apply (rule admD [OF adm])
apply (simp add: chain_basis_fun_take)
apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
apply (clarify, simp add: P)
@@ -452,7 +452,7 @@
lemma compacts_lessD: "compacts x \<subseteq> compacts y \<Longrightarrow> x \<sqsubseteq> y"
apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
-apply (rule admD [rule_format], simp, simp)
+apply (rule admD, simp, simp)
apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
apply (simp add: compacts_def Abs_compact_basis_inverse)
--- a/src/HOLCF/ConvexPD.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy Fri Jan 18 20:22:07 2008 +0100
@@ -372,7 +372,7 @@
apply (rule iffI)
apply (subgoal_tac
"adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
- apply (drule admD [rule_format], rule chain_approx)
+ apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
@@ -391,7 +391,7 @@
apply (rule iffI)
apply (subgoal_tac
"adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
- apply (drule admD [rule_format], rule chain_approx)
+ apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
--- a/src/HOLCF/Fix.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Fix.thy Fri Jan 18 20:22:07 2008 +0100
@@ -153,7 +153,7 @@
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
apply (subst fix_def2)
-apply (erule admD [rule_format])
+apply (erule admD)
apply (rule chain_iterate)
apply (induct_tac "i", simp_all)
done
@@ -233,7 +233,7 @@
apply (intro strip)
apply (erule admD)
apply (rule chain_iterate)
-apply assumption
+apply (erule spec)
done
text {* computational induction for weak admissible formulae *}
--- a/src/HOLCF/LowerPD.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/LowerPD.thy Fri Jan 18 20:22:07 2008 +0100
@@ -376,7 +376,7 @@
apply (rule iffI)
apply (subgoal_tac
"adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
- apply (drule admD [rule_format], rule chain_approx)
+ apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
--- a/src/HOLCF/Pcpodef.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy Fri Jan 18 20:22:07 2008 +0100
@@ -104,7 +104,7 @@
and adm: "adm (\<lambda>x. x \<in> A)"
shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])
+ apply (erule admD [OF adm ch2ch_Rep [OF less]])
apply (rule type_definition.Rep [OF type])
done
--- a/src/HOLCF/UpperPD.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/UpperPD.thy Fri Jan 18 20:22:07 2008 +0100
@@ -346,7 +346,7 @@
apply (rule iffI)
apply (subgoal_tac
"adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
- apply (drule admD [rule_format], rule chain_approx)
+ apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)