# HG changeset patch
# User wenzelm
# Date 1321819626 -3600
# Node ID b1e1508643b1914410cc4dddf74239f8b1fe0db4
# Parent  a89b4bc311a53064ebcab25bbbc064b0449aed58
eliminated obsolete "standard";

diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/Cfun.thy
--- 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 *}
 
diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/ConvexPD.thy
--- 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
diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/Cpodef.thy
--- 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"
diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- 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"
diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- 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:
diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- 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 *)
diff -r a89b4bc311a5 -r b1e1508643b1 src/HOL/HOLCF/ex/Hoare.thy
--- 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"