--- a/src/HOL/HOLCF/Cfun.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Sun Nov 20 21:07:06 2011 +0100
@@ -194,8 +194,8 @@
lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
-lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
-lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono]
+lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono]
text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
--- a/src/HOL/HOLCF/ConvexPD.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Sun Nov 20 21:07:06 2011 +0100
@@ -609,7 +609,8 @@
done
lemmas convex_plus_below_plus_iff =
- convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws", standard]
+ convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws"]
+ for xs ys zs ws
lemmas convex_pd_below_simps =
convex_unit_below_plus_iff
--- a/src/HOL/HOLCF/Cpodef.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy Sun Nov 20 21:07:06 2011 +0100
@@ -107,7 +107,7 @@
by (rule typedef_is_lubI [OF below])
qed
-lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
+lemmas typedef_lub = typedef_is_lub [THEN lub_eqI]
theorem typedef_cpo:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Sun Nov 20 21:07:06 2011 +0100
@@ -353,8 +353,8 @@
apply blast
done
-lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act, standard]
-lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act, standard]
+lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
+lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
lemma intA_is_not_extB:
"[| compatible A B; x:int A |] ==> x~:ext B"
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Sun Nov 20 21:07:06 2011 +0100
@@ -249,8 +249,8 @@
apply blast
done
-lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1, standard]
-lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard]
+lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1]
+lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2]
lemma trace_inclusion_for_simulations:
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Sun Nov 20 21:07:06 2011 +0100
@@ -402,7 +402,7 @@
done
lemmas exec_prefixclosed =
- conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard]
+ conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]]
(* second prefix notion for Finite x *)
--- a/src/HOL/HOLCF/ex/Hoare.thy Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/ex/Hoare.thy Sun Nov 20 21:07:06 2011 +0100
@@ -155,8 +155,6 @@
(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
-thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
-
lemma hoare_lemma10:
"EX k. b1$(iterate k$g$x) ~= TT
==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"