eliminated obsolete "standard";
authorwenzelm
Sun Nov 20 21:07:06 2011 +0100 (2011-11-20)
changeset 45606b1e1508643b1
parent 45605 a89b4bc311a5
child 45607 16b4f5774621
eliminated obsolete "standard";
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/HOLCF/ex/Hoare.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 20 21:05:23 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 20 21:07:06 2011 +0100
     1.3 @@ -194,8 +194,8 @@
     1.4  
     1.5  lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
     1.6  
     1.7 -lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
     1.8 -lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
     1.9 +lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono]
    1.10 +lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono]
    1.11  
    1.12  text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
    1.13  
     2.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Nov 20 21:05:23 2011 +0100
     2.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Nov 20 21:07:06 2011 +0100
     2.3 @@ -609,7 +609,8 @@
     2.4  done
     2.5  
     2.6  lemmas convex_plus_below_plus_iff =
     2.7 -  convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws", standard]
     2.8 +  convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws"]
     2.9 +  for xs ys zs ws
    2.10  
    2.11  lemmas convex_pd_below_simps =
    2.12    convex_unit_below_plus_iff
     3.1 --- a/src/HOL/HOLCF/Cpodef.thy	Sun Nov 20 21:05:23 2011 +0100
     3.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Sun Nov 20 21:07:06 2011 +0100
     3.3 @@ -107,7 +107,7 @@
     3.4      by (rule typedef_is_lubI [OF below])
     3.5  qed
     3.6  
     3.7 -lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
     3.8 +lemmas typedef_lub = typedef_is_lub [THEN lub_eqI]
     3.9  
    3.10  theorem typedef_cpo:
    3.11    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
     4.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 20 21:05:23 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 20 21:07:06 2011 +0100
     4.3 @@ -353,8 +353,8 @@
     4.4  apply blast
     4.5  done
     4.6  
     4.7 -lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act, standard]
     4.8 -lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act, standard]
     4.9 +lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
    4.10 +lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
    4.11  
    4.12  lemma intA_is_not_extB: 
    4.13   "[| compatible A B; x:int A |] ==> x~:ext B"
     5.1 --- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sun Nov 20 21:05:23 2011 +0100
     5.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sun Nov 20 21:07:06 2011 +0100
     5.3 @@ -249,8 +249,8 @@
     5.4    apply blast
     5.5    done
     5.6  
     5.7 -lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1, standard]
     5.8 -lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard]
     5.9 +lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1]
    5.10 +lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2]
    5.11  
    5.12  
    5.13  lemma trace_inclusion_for_simulations:
     6.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sun Nov 20 21:05:23 2011 +0100
     6.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sun Nov 20 21:07:06 2011 +0100
     6.3 @@ -402,7 +402,7 @@
     6.4  done
     6.5  
     6.6  lemmas exec_prefixclosed =
     6.7 -  conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard]
     6.8 +  conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]]
     6.9  
    6.10  
    6.11  (* second prefix notion for Finite x *)
     7.1 --- a/src/HOL/HOLCF/ex/Hoare.thy	Sun Nov 20 21:05:23 2011 +0100
     7.2 +++ b/src/HOL/HOLCF/ex/Hoare.thy	Sun Nov 20 21:07:06 2011 +0100
     7.3 @@ -155,8 +155,6 @@
     7.4  
     7.5  (* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
     7.6  
     7.7 -thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
     7.8 -
     7.9  lemma hoare_lemma10:
    7.10    "EX k. b1$(iterate k$g$x) ~= TT
    7.11      ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"