eliminated obsolete "standard";
authorwenzelm
Sun Nov 20 21:05:23 2011 +0100 (2011-11-20)
changeset 45605a89b4bc311a5
parent 45604 29cf40fe8daf
child 45606 b1e1508643b1
eliminated obsolete "standard";
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/WellForm.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
src/HOL/IMP/Comp_Rev.thy
src/HOL/IMPP/Hoare.thy
src/HOL/Induct/PropLog.thy
src/HOL/Induct/SList.thy
src/HOL/Library/AList.thy
src/HOL/Library/Polynomial.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/NSA/Examples/NSPrimes.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/StarDef.thy
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/EulerFermat.thy
src/HOL/Old_Number_Theory/WilsonBij.thy
src/HOL/Proofs/Lambda/NormalForm.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/SET_Protocol/Event_SET.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/TLA.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Rename.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
src/HOL/ex/Gauge_Integration.thy
src/HOL/ex/Tree23.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4  (*Simplifying   
     1.5   parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
     1.6    This version won't loop with the simplifier.*)
     1.7 -lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
     1.8 +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
     1.9  
    1.10  lemma knows_Spy_Says [simp]:
    1.11       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    1.12 @@ -138,10 +138,10 @@
    1.13  text{*Elimination rules: derive contradictions from old Says events containing
    1.14    items known to be fresh*}
    1.15  lemmas Says_imp_parts_knows_Spy = 
    1.16 -       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
    1.17 +       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl] 
    1.18  
    1.19  lemmas knows_Spy_partsEs =
    1.20 -     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
    1.21 +     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
    1.22  
    1.23  lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
    1.24  
    1.25 @@ -278,7 +278,7 @@
    1.26      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
    1.27  
    1.28  
    1.29 -lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
    1.30 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
    1.31  
    1.32  ML
    1.33  {*
    1.34 @@ -294,7 +294,7 @@
    1.35  
    1.36  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.37  
    1.38 -lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
    1.39 +lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
    1.40  
    1.41  ML
    1.42  {*
     2.1 --- a/src/HOL/Auth/Message.thy	Sun Nov 20 20:59:30 2011 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Sun Nov 20 21:05:23 2011 +0100
     2.3 @@ -166,7 +166,7 @@
     2.4  lemma parts_increasing: "H \<subseteq> parts(H)"
     2.5  by blast
     2.6  
     2.7 -lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
     2.8 +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
     2.9  
    2.10  lemma parts_empty [simp]: "parts{} = {}"
    2.11  apply safe
    2.12 @@ -358,9 +358,9 @@
    2.13  apply (erule analz.induct, blast+)
    2.14  done
    2.15  
    2.16 -lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
    2.17 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
    2.18  
    2.19 -lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
    2.20 +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
    2.21  
    2.22  
    2.23  lemma parts_analz [simp]: "parts (analz H) = parts H"
    2.24 @@ -371,7 +371,7 @@
    2.25  apply (erule analz.induct, auto)
    2.26  done
    2.27  
    2.28 -lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
    2.29 +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
    2.30  
    2.31  subsubsection{*General equational properties *}
    2.32  
    2.33 @@ -790,21 +790,23 @@
    2.34  text{*Rewrites to push in Key and Crypt messages, so that other messages can
    2.35      be pulled out using the @{text analz_insert} rules*}
    2.36  
    2.37 -lemmas pushKeys [standard] =
    2.38 +lemmas pushKeys =
    2.39    insert_commute [of "Key K" "Agent C"]
    2.40    insert_commute [of "Key K" "Nonce N"]
    2.41    insert_commute [of "Key K" "Number N"]
    2.42    insert_commute [of "Key K" "Hash X"]
    2.43    insert_commute [of "Key K" "MPair X Y"]
    2.44    insert_commute [of "Key K" "Crypt X K'"]
    2.45 +  for K C N X Y K'
    2.46  
    2.47 -lemmas pushCrypts [standard] =
    2.48 +lemmas pushCrypts =
    2.49    insert_commute [of "Crypt X K" "Agent C"]
    2.50    insert_commute [of "Crypt X K" "Agent C"]
    2.51    insert_commute [of "Crypt X K" "Nonce N"]
    2.52    insert_commute [of "Crypt X K" "Number N"]
    2.53    insert_commute [of "Crypt X K" "Hash X'"]
    2.54    insert_commute [of "Crypt X K" "MPair X' Y"]
    2.55 +  for X K C N X' Y
    2.56  
    2.57  text{*Cannot be added with @{text "[simp]"} -- messages should not always be
    2.58    re-ordered. *}
     3.1 --- a/src/HOL/Auth/OtwayRees.thy	Sun Nov 20 20:59:30 2011 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees.thy	Sun Nov 20 21:05:23 2011 +0100
     3.3 @@ -121,7 +121,7 @@
     3.4    We can replace them by rewriting with parts_insert2 and proving using
     3.5    dest: parts_cut, but the proofs become more difficult.*)
     3.6  lemmas OR2_parts_knows_Spy =
     3.7 -    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
     3.8 +    OR2_analz_knows_Spy [THEN analz_into_parts]
     3.9  
    3.10  (*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
    3.11    some reason proofs work without them!*)
     4.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Sun Nov 20 20:59:30 2011 +0100
     4.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Sun Nov 20 21:05:23 2011 +0100
     4.3 @@ -122,7 +122,7 @@
     4.4  by blast
     4.5  
     4.6  lemmas OR2_parts_knows_Spy =
     4.7 -    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
     4.8 +    OR2_analz_knows_Spy [THEN analz_into_parts]
     4.9  
    4.10  ML
    4.11  {*
     5.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Sun Nov 20 20:59:30 2011 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sun Nov 20 21:05:23 2011 +0100
     5.3 @@ -128,7 +128,7 @@
     5.4  
     5.5  text{*Forwarding lemma: see comments in OtwayRees.thy*}
     5.6  lemmas OR2_parts_knows_Spy =
     5.7 -    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
     5.8 +    OR2_analz_knows_Spy [THEN analz_into_parts]
     5.9  
    5.10  
    5.11  text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
     6.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Sun Nov 20 20:59:30 2011 +0100
     6.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Sun Nov 20 21:05:23 2011 +0100
     6.3 @@ -118,7 +118,7 @@
     6.4  (*Simplifying   
     6.5   parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
     6.6    This version won't loop with the simplifier.*)
     6.7 -lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
     6.8 +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
     6.9  
    6.10  lemma knows_Spy_Says [simp]:
    6.11       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    6.12 @@ -237,8 +237,8 @@
    6.13  text{*Elimination rules: derive contradictions from old Says events containing
    6.14    items known to be fresh*}
    6.15  lemmas knows_Spy_partsEs =
    6.16 -     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
    6.17 -     parts.Body [THEN revcut_rl, standard]
    6.18 +     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
    6.19 +     parts.Body [THEN revcut_rl]
    6.20  
    6.21  
    6.22  
     7.1 --- a/src/HOL/Auth/Yahalom.thy	Sun Nov 20 20:59:30 2011 +0100
     7.2 +++ b/src/HOL/Auth/Yahalom.thy	Sun Nov 20 21:05:23 2011 +0100
     7.3 @@ -121,7 +121,7 @@
     7.4  by blast
     7.5  
     7.6  lemmas YM4_parts_knows_Spy =
     7.7 -       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
     7.8 +       YM4_analz_knows_Spy [THEN analz_into_parts]
     7.9  
    7.10  text{*For Oops*}
    7.11  lemma YM4_Key_parts_knows_Spy:
     8.1 --- a/src/HOL/Auth/Yahalom2.thy	Sun Nov 20 20:59:30 2011 +0100
     8.2 +++ b/src/HOL/Auth/Yahalom2.thy	Sun Nov 20 21:05:23 2011 +0100
     8.3 @@ -116,7 +116,7 @@
     8.4  by blast
     8.5  
     8.6  lemmas YM4_parts_knows_Spy =
     8.7 -       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
     8.8 +       YM4_analz_knows_Spy [THEN analz_into_parts]
     8.9  
    8.10  
    8.11  (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
     9.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Sun Nov 20 20:59:30 2011 +0100
     9.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Sun Nov 20 21:05:23 2011 +0100
     9.3 @@ -103,7 +103,7 @@
     9.4  by blast
     9.5  
     9.6  lemmas YM4_parts_knows_Spy =
     9.7 -       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
     9.8 +       YM4_analz_knows_Spy [THEN analz_into_parts]
     9.9  
    9.10  
    9.11  text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
    10.1 --- a/src/HOL/Bali/AxCompl.thy	Sun Nov 20 20:59:30 2011 +0100
    10.2 +++ b/src/HOL/Bali/AxCompl.thy	Sun Nov 20 21:05:23 2011 +0100
    10.3 @@ -30,7 +30,7 @@
    10.4  done
    10.5  
    10.6  lemmas finite_nyinitcls [simp] =
    10.7 -   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
    10.8 +   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset]]
    10.9  
   10.10  lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
   10.11  apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
    11.1 --- a/src/HOL/Bali/AxSem.thy	Sun Nov 20 20:59:30 2011 +0100
    11.2 +++ b/src/HOL/Bali/AxSem.thy	Sun Nov 20 21:05:23 2011 +0100
    11.3 @@ -1016,7 +1016,7 @@
    11.4  apply  (rule ax_derivs.Skip)
    11.5  apply fast
    11.6  done
    11.7 -lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
    11.8 +lemmas ax_SkipI = ax_Skip [THEN conseq1]
    11.9  
   11.10  
   11.11  section "derived rules for methd call"
    12.1 --- a/src/HOL/Bali/Decl.thy	Sun Nov 20 20:59:30 2011 +0100
    12.2 +++ b/src/HOL/Bali/Decl.thy	Sun Nov 20 21:05:23 2011 +0100
    12.3 @@ -613,8 +613,8 @@
    12.4  apply auto
    12.5  done
    12.6  
    12.7 -lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
    12.8 -lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
    12.9 +lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI]
   12.10 +lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
   12.11  
   12.12  
   12.13  lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
    13.1 --- a/src/HOL/Bali/Table.thy	Sun Nov 20 20:59:30 2011 +0100
    13.2 +++ b/src/HOL/Bali/Table.thy	Sun Nov 20 21:05:23 2011 +0100
    13.3 @@ -222,7 +222,7 @@
    13.4  apply auto
    13.5  done
    13.6  
    13.7 -lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
    13.8 +lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI]
    13.9  
   13.10  lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
   13.11     table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
    14.1 --- a/src/HOL/Bali/TypeRel.thy	Sun Nov 20 20:59:30 2011 +0100
    14.2 +++ b/src/HOL/Bali/TypeRel.thy	Sun Nov 20 21:05:23 2011 +0100
    14.3 @@ -60,7 +60,7 @@
    14.4    (* direct subinterface in Decl.thy, cf. 9.1.3 *)
    14.5    (* direct subclass     in Decl.thy, cf. 8.1.3 *)
    14.6  
    14.7 -lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]
    14.8 +lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
    14.9  
   14.10  lemma subcls_direct1:
   14.11   "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"
   14.12 @@ -554,9 +554,9 @@
   14.13  done
   14.14  
   14.15  lemmas subint_antisym = 
   14.16 -       subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
   14.17 +       subint1_acyclic [THEN acyclic_impl_antisym_rtrancl]
   14.18  lemmas subcls_antisym = 
   14.19 -       subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
   14.20 +       subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl]
   14.21  
   14.22  lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
   14.23  by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
    15.1 --- a/src/HOL/Bali/WellForm.thy	Sun Nov 20 20:59:30 2011 +0100
    15.2 +++ b/src/HOL/Bali/WellForm.thy	Sun Nov 20 21:05:23 2011 +0100
    15.3 @@ -739,7 +739,7 @@
    15.4  proof -
    15.5    assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
    15.6  
    15.7 -  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
    15.8 +  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]  (* FIXME !? *)
    15.9    have "wf_prog G \<longrightarrow> 
   15.10           (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
   15.11                    \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
   15.12 @@ -1355,7 +1355,7 @@
   15.13    qed
   15.14  qed
   15.15  
   15.16 -lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
   15.17 +lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P
   15.18  
   15.19  lemma declclass_widen[rule_format]: 
   15.20   "wf_prog G 
    16.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Nov 20 20:59:30 2011 +0100
    16.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Nov 20 21:05:23 2011 +0100
    16.3 @@ -281,7 +281,7 @@
    16.4  apply (drule_tac x = m in spec)
    16.5  apply (auto simp add:field_simps)
    16.6  done
    16.7 -lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard]
    16.8 +lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0]
    16.9  
   16.10  lemma poly_roots_index_length0: "poly p (x::'a::idom) \<noteq> poly [] x ==>
   16.11        \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
   16.12 @@ -322,7 +322,7 @@
   16.13  apply (clarsimp simp add: field_simps)
   16.14  done
   16.15  
   16.16 -lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
   16.17 +lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma]
   16.18  
   16.19  lemma poly_roots_index_length: "poly p (x::'a::idom) \<noteq> poly [] x ==>
   16.20        \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
    17.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Nov 20 20:59:30 2011 +0100
    17.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Nov 20 21:05:23 2011 +0100
    17.3 @@ -24,7 +24,7 @@
    17.4    elements of the chain.
    17.5  *}
    17.6  lemmas [dest?] = chainD
    17.7 -lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
    17.8 +lemmas chainE2 [elim?] = chainD2 [elim_format]
    17.9  
   17.10  lemma some_H'h't:
   17.11    assumes M: "M = norm_pres_extensions E p F f"
    18.1 --- a/src/HOL/IMP/Comp_Rev.thy	Sun Nov 20 20:59:30 2011 +0100
    18.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Sun Nov 20 21:05:23 2011 +0100
    18.3 @@ -363,7 +363,7 @@
    18.4  qed
    18.5  
    18.6  lemmas exec_n_drop_Cons = 
    18.7 -  exec_n_drop_left [where P="[instr]", simplified, standard]
    18.8 +  exec_n_drop_left [where P="[instr]", simplified] for instr
    18.9  
   18.10  definition
   18.11    "closed P \<longleftrightarrow> exits P \<subseteq> {isize P}" 
    19.1 --- a/src/HOL/IMPP/Hoare.thy	Sun Nov 20 20:59:30 2011 +0100
    19.2 +++ b/src/HOL/IMPP/Hoare.thy	Sun Nov 20 21:05:23 2011 +0100
    19.3 @@ -460,7 +460,7 @@
    19.4  done
    19.5  
    19.6  (* requires Body+empty+insert / BodyN, com_det *)
    19.7 -lemmas hoare_complete = MGF' [THEN MGF_complete, standard]
    19.8 +lemmas hoare_complete = MGF' [THEN MGF_complete]
    19.9  
   19.10  
   19.11  subsection "unused derived rules"
    20.1 --- a/src/HOL/Induct/PropLog.thy	Sun Nov 20 20:59:30 2011 +0100
    20.2 +++ b/src/HOL/Induct/PropLog.thy	Sun Nov 20 21:05:23 2011 +0100
    20.3 @@ -111,7 +111,7 @@
    20.4  
    20.5  lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
    20.6  
    20.7 -lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
    20.8 +lemmas thms_notE = thms.MP [THEN thms_falseE]
    20.9  
   20.10  
   20.11  subsubsection {* Soundness of the rules wrt truth-table semantics *}
    21.1 --- a/src/HOL/Induct/SList.thy	Sun Nov 20 20:59:30 2011 +0100
    21.2 +++ b/src/HOL/Induct/SList.thy	Sun Nov 20 21:05:23 2011 +0100
    21.3 @@ -191,7 +191,7 @@
    21.4  by (simp add: NIL_def CONS_def)
    21.5  
    21.6  lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
    21.7 -lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
    21.8 +lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE]
    21.9  lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
   21.10  
   21.11  lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
   21.12 @@ -200,8 +200,9 @@
   21.13  apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
   21.14  done
   21.15  
   21.16 -lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
   21.17 -lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
   21.18 +lemmas Nil_not_Cons = Cons_not_Nil [THEN not_sym]
   21.19 +declare Nil_not_Cons [iff]
   21.20 +lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE]
   21.21  lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
   21.22  
   21.23  (** Injectiveness of CONS and Cons **)
   21.24 @@ -220,7 +221,7 @@
   21.25  apply (auto simp add: Rep_List_inject)
   21.26  done
   21.27  
   21.28 -lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
   21.29 +lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
   21.30  
   21.31  lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
   21.32    by (induct L == "CONS M N" set: list) auto
   21.33 @@ -264,8 +265,7 @@
   21.34  by (simp add: List_rec_def)
   21.35  
   21.36  lemmas List_rec_unfold = 
   21.37 -    def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl], 
   21.38 -               standard]
   21.39 +    def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl]]
   21.40  
   21.41  
   21.42  (** pred_sexp lemmas **)
    22.1 --- a/src/HOL/Library/AList.thy	Sun Nov 20 20:59:30 2011 +0100
    22.2 +++ b/src/HOL/Library/AList.thy	Sun Nov 20 21:05:23 2011 +0100
    22.3 @@ -467,7 +467,7 @@
    22.4    (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
    22.5    by (simp add: merge_conv' map_add_Some_iff)
    22.6  
    22.7 -lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
    22.8 +lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
    22.9  
   22.10  lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   22.11    by (simp add: merge_conv')
    23.1 --- a/src/HOL/Library/Polynomial.thy	Sun Nov 20 20:59:30 2011 +0100
    23.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Nov 20 21:05:23 2011 +0100
    23.3 @@ -928,11 +928,9 @@
    23.4  lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
    23.5  by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
    23.6  
    23.7 -lemmas pdivmod_rel_unique_div =
    23.8 -  pdivmod_rel_unique [THEN conjunct1, standard]
    23.9 +lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
   23.10  
   23.11 -lemmas pdivmod_rel_unique_mod =
   23.12 -  pdivmod_rel_unique [THEN conjunct2, standard]
   23.13 +lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
   23.14  
   23.15  instantiation poly :: (field) ring_div
   23.16  begin
    24.1 --- a/src/HOL/Metis_Examples/Message.thy	Sun Nov 20 20:59:30 2011 +0100
    24.2 +++ b/src/HOL/Metis_Examples/Message.thy	Sun Nov 20 21:05:23 2011 +0100
    24.3 @@ -164,7 +164,7 @@
    24.4  lemma parts_increasing: "H \<subseteq> parts(H)"
    24.5  by blast
    24.6  
    24.7 -lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
    24.8 +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
    24.9  
   24.10  lemma parts_empty [simp]: "parts{} = {}"
   24.11  apply safe
   24.12 @@ -353,9 +353,9 @@
   24.13  apply (erule analz.induct, blast+)
   24.14  done
   24.15  
   24.16 -lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   24.17 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
   24.18  
   24.19 -lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   24.20 +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
   24.21  
   24.22  lemma parts_analz [simp]: "parts (analz H) = parts H"
   24.23  apply (rule equalityI)
   24.24 @@ -369,7 +369,7 @@
   24.25  apply (erule analz.induct, auto)
   24.26  done
   24.27  
   24.28 -lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   24.29 +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
   24.30  
   24.31  subsubsection{*General equational properties *}
   24.32  
    25.1 --- a/src/HOL/MicroJava/BV/JType.thy	Sun Nov 20 20:59:30 2011 +0100
    25.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Sun Nov 20 21:05:23 2011 +0100
    25.3 @@ -142,7 +142,7 @@
    25.4  apply (case_tac t)
    25.5   apply simp
    25.6  apply simp
    25.7 -apply (insert rtrancl_r_diff_Id [symmetric, standard, of "subcls1 G"])
    25.8 +apply (insert rtrancl_r_diff_Id [symmetric, of "subcls1 G"])
    25.9  apply simp
   25.10  apply (erule rtrancl.cases)
   25.11   apply blast
    26.1 --- a/src/HOL/MicroJava/J/Example.thy	Sun Nov 20 20:59:30 2011 +0100
    26.2 +++ b/src/HOL/MicroJava/J/Example.thy	Sun Nov 20 21:05:23 2011 +0100
    26.3 @@ -202,7 +202,7 @@
    26.4  apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
    26.5  done
    26.6  
    26.7 -lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"], standard]
    26.8 +lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"]] for G
    26.9  
   26.10  lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
   26.11  apply (rule subcls_direct)
    27.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 20 20:59:30 2011 +0100
    27.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 20 21:05:23 2011 +0100
    27.3 @@ -141,22 +141,22 @@
    27.4    done
    27.5  
    27.6  lemmas scaleR_right_has_derivative =
    27.7 -  bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
    27.8 +  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
    27.9  
   27.10  lemmas scaleR_left_has_derivative =
   27.11 -  bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
   27.12 +  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
   27.13  
   27.14  lemmas inner_right_has_derivative =
   27.15 -  bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
   27.16 +  bounded_linear.has_derivative [OF bounded_linear_inner_right]
   27.17  
   27.18  lemmas inner_left_has_derivative =
   27.19 -  bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
   27.20 +  bounded_linear.has_derivative [OF bounded_linear_inner_left]
   27.21  
   27.22  lemmas mult_right_has_derivative =
   27.23 -  bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
   27.24 +  bounded_linear.has_derivative [OF bounded_linear_mult_right]
   27.25  
   27.26  lemmas mult_left_has_derivative =
   27.27 -  bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
   27.28 +  bounded_linear.has_derivative [OF bounded_linear_mult_left]
   27.29  
   27.30  lemmas euclidean_component_has_derivative =
   27.31    bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
    28.1 --- a/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 20 20:59:30 2011 +0100
    28.2 +++ b/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 20 21:05:23 2011 +0100
    28.3 @@ -39,7 +39,7 @@
    28.4  apply (force intro!: dvd_mult)
    28.5  done
    28.6  
    28.7 -lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
    28.8 +lemmas dvd_by_all2 = dvd_by_all [THEN spec]
    28.9  
   28.10  lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
   28.11  by (transfer, simp)
   28.12 @@ -50,7 +50,7 @@
   28.13  lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
   28.14  by (transfer, rule dvd_by_all)
   28.15  
   28.16 -lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
   28.17 +lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]
   28.18  
   28.19  (* Goldblatt: Exercise 5.11(2) - p. 57 *)
   28.20  lemma hypnat_dvd_all_hypnat_of_nat:
    29.1 --- a/src/HOL/NSA/HyperDef.thy	Sun Nov 20 20:59:30 2011 +0100
    29.2 +++ b/src/HOL/NSA/HyperDef.thy	Sun Nov 20 21:05:23 2011 +0100
    29.3 @@ -422,7 +422,7 @@
    29.4  lemma power_hypreal_of_real_number_of:
    29.5       "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
    29.6  by simp
    29.7 -declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
    29.8 +declare power_hypreal_of_real_number_of [of _ "number_of w", simp] for w
    29.9  (*
   29.10  lemma hrealpow_HFinite:
   29.11    fixes x :: "'a::{real_normed_algebra,power} star"
    30.1 --- a/src/HOL/NSA/StarDef.thy	Sun Nov 20 20:59:30 2011 +0100
    30.2 +++ b/src/HOL/NSA/StarDef.thy	Sun Nov 20 21:05:23 2011 +0100
    30.3 @@ -683,18 +683,18 @@
    30.4  text{*As above, for numerals*}
    30.5  
    30.6  lemmas star_of_number_less =
    30.7 -  star_of_less [of "number_of w", standard, simplified star_of_number_of]
    30.8 +  star_of_less [of "number_of w", simplified star_of_number_of] for w
    30.9  lemmas star_of_number_le   =
   30.10 -  star_of_le   [of "number_of w", standard, simplified star_of_number_of]
   30.11 +  star_of_le   [of "number_of w", simplified star_of_number_of] for w
   30.12  lemmas star_of_number_eq   =
   30.13 -  star_of_eq   [of "number_of w", standard, simplified star_of_number_of]
   30.14 +  star_of_eq   [of "number_of w", simplified star_of_number_of] for w
   30.15  
   30.16  lemmas star_of_less_number =
   30.17 -  star_of_less [of _ "number_of w", standard, simplified star_of_number_of]
   30.18 +  star_of_less [of _ "number_of w", simplified star_of_number_of] for w
   30.19  lemmas star_of_le_number   =
   30.20 -  star_of_le   [of _ "number_of w", standard, simplified star_of_number_of]
   30.21 +  star_of_le   [of _ "number_of w", simplified star_of_number_of] for w
   30.22  lemmas star_of_eq_number   =
   30.23 -  star_of_eq   [of _ "number_of w", standard, simplified star_of_number_of]
   30.24 +  star_of_eq   [of _ "number_of w", simplified star_of_number_of] for w
   30.25  
   30.26  lemmas star_of_simps [simp] =
   30.27    star_of_add     star_of_diff    star_of_minus
    31.1 --- a/src/HOL/NanoJava/AxSem.thy	Sun Nov 20 20:59:30 2011 +0100
    31.2 +++ b/src/HOL/NanoJava/AxSem.thy	Sun Nov 20 21:05:23 2011 +0100
    31.3 @@ -196,6 +196,6 @@
    31.4  apply (auto del: image_eqI intro: rev_image_eqI)
    31.5  done
    31.6  
    31.7 -lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard]
    31.8 +lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm
    31.9  
   31.10  end
    32.1 --- a/src/HOL/NanoJava/TypeRel.thy	Sun Nov 20 20:59:30 2011 +0100
    32.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Sun Nov 20 21:05:23 2011 +0100
    32.3 @@ -86,7 +86,7 @@
    32.4  apply auto
    32.5  done
    32.6  
    32.7 -lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
    32.8 +lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
    32.9  
   32.10  lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
   32.11  by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
    33.1 --- a/src/HOL/Number_Theory/Primes.thy	Sun Nov 20 20:59:30 2011 +0100
    33.2 +++ b/src/HOL/Number_Theory/Primes.thy	Sun Nov 20 21:05:23 2011 +0100
    33.3 @@ -206,7 +206,7 @@
    33.4      "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
    33.5    by (auto simp add: prime_nat_code)
    33.6  
    33.7 -lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
    33.8 +lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m"] for m
    33.9  
   33.10  lemma prime_int_code [code]:
   33.11    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   33.12 @@ -222,7 +222,7 @@
   33.13  lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   33.14    by (auto simp add: prime_int_code)
   33.15  
   33.16 -lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
   33.17 +lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m"] for m
   33.18  
   33.19  lemma two_is_prime_nat [simp]: "prime (2::nat)"
   33.20    by simp
    34.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 20 20:59:30 2011 +0100
    34.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 20 21:05:23 2011 +0100
    34.3 @@ -196,10 +196,8 @@
    34.4    apply (rule aux_some, simp_all)
    34.5    done
    34.6  
    34.7 -lemmas RRset2norRR_correct1 =
    34.8 -  RRset2norRR_correct [THEN conjunct1, standard]
    34.9 -lemmas RRset2norRR_correct2 =
   34.10 -  RRset2norRR_correct [THEN conjunct2, standard]
   34.11 +lemmas RRset2norRR_correct1 = RRset2norRR_correct [THEN conjunct1]
   34.12 +lemmas RRset2norRR_correct2 = RRset2norRR_correct [THEN conjunct2]
   34.13  
   34.14  lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
   34.15    by (induct set: RsetR) auto
    35.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Nov 20 20:59:30 2011 +0100
    35.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Nov 20 21:05:23 2011 +0100
    35.3 @@ -41,9 +41,9 @@
    35.4      apply auto
    35.5    done
    35.6  
    35.7 -lemmas inv_ge = inv_correct [THEN conjunct1, standard]
    35.8 -lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1, standard]
    35.9 -lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard]
   35.10 +lemmas inv_ge = inv_correct [THEN conjunct1]
   35.11 +lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1]
   35.12 +lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2]
   35.13  
   35.14  lemma inv_not_0:
   35.15    "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
    36.1 --- a/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 20:59:30 2011 +0100
    36.2 +++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 21:05:23 2011 +0100
    36.3 @@ -132,10 +132,10 @@
    36.4    apply (drule listall_conj2)
    36.5    apply (drule_tac i=i and j=j in subst_terms_NF)
    36.6    apply assumption
    36.7 -  apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])
    36.8 +  apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
    36.9    apply simp
   36.10    apply (erule NF.App)
   36.11 -  apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
   36.12 +  apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
   36.13    apply simp
   36.14    apply (iprover intro: NF.App)
   36.15    apply simp
   36.16 @@ -173,7 +173,7 @@
   36.17    apply (drule listall_conj2)
   36.18    apply (drule_tac i=i in lift_terms_NF)
   36.19    apply assumption
   36.20 -  apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])
   36.21 +  apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
   36.22    apply simp
   36.23    apply (rule NF.App)
   36.24    apply assumption
    37.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Sun Nov 20 20:59:30 2011 +0100
    37.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Sun Nov 20 21:05:23 2011 +0100
    37.3 @@ -649,8 +649,8 @@
    37.4  subsection {* union_fset *}
    37.5  
    37.6  lemmas [simp] =
    37.7 -  sup_bot_left[where 'a="'a fset", standard]
    37.8 -  sup_bot_right[where 'a="'a fset", standard]
    37.9 +  sup_bot_left[where 'a="'a fset"]
   37.10 +  sup_bot_right[where 'a="'a fset"]
   37.11  
   37.12  lemma union_insert_fset [simp]:
   37.13    shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)"
    38.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Nov 20 20:59:30 2011 +0100
    38.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Nov 20 21:05:23 2011 +0100
    38.3 @@ -263,11 +263,12 @@
    38.4  qed
    38.5  
    38.6  lemmas int_distrib =
    38.7 -  left_distrib [of "z1::int" "z2" "w", standard]
    38.8 -  right_distrib [of "w::int" "z1" "z2", standard]
    38.9 -  left_diff_distrib [of "z1::int" "z2" "w", standard]
   38.10 -  right_diff_distrib [of "w::int" "z1" "z2", standard]
   38.11 -  minus_add_distrib[of "z1::int" "z2", standard]
   38.12 +  left_distrib [of z1 z2 w]
   38.13 +  right_distrib [of w z1 z2]
   38.14 +  left_diff_distrib [of z1 z2 w]
   38.15 +  right_diff_distrib [of w z1 z2]
   38.16 +  minus_add_distrib[of z1 z2]
   38.17 +  for z1 z2 w :: int
   38.18  
   38.19  lemma int_induct_raw:
   38.20    assumes a: "P (0::nat, 0)"
    39.1 --- a/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 20 20:59:30 2011 +0100
    39.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 20 21:05:23 2011 +0100
    39.3 @@ -82,7 +82,7 @@
    39.4  (** Simplifying   parts (insert X (knows Spy evs))
    39.5        = parts {X} Un parts (knows Spy evs) -- since general case loops*)
    39.6  
    39.7 -lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
    39.8 +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
    39.9  
   39.10  lemma knows_Spy_Says [simp]:
   39.11       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
   39.12 @@ -126,8 +126,8 @@
   39.13  (*Use with addSEs to derive contradictions from old Says events containing
   39.14    items known to be fresh*)
   39.15  lemmas knows_Spy_partsEs =
   39.16 -     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
   39.17 -     parts.Body [THEN revcut_rl, standard]
   39.18 +     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl] 
   39.19 +     parts.Body [THEN revcut_rl]
   39.20  
   39.21  
   39.22  subsection{*The Function @{term used}*}
   39.23 @@ -177,7 +177,7 @@
   39.24         knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
   39.25         knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
   39.26  
   39.27 -lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
   39.28 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
   39.29  
   39.30  ML
   39.31  {*
    40.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Sun Nov 20 20:59:30 2011 +0100
    40.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Sun Nov 20 21:05:23 2011 +0100
    40.3 @@ -210,7 +210,7 @@
    40.4  lemma parts_increasing: "H \<subseteq> parts(H)"
    40.5  by blast
    40.6  
    40.7 -lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
    40.8 +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
    40.9  
   40.10  lemma parts_empty [simp]: "parts{} = {}"
   40.11  apply safe
   40.12 @@ -424,9 +424,9 @@
   40.13  apply (erule analz.induct, blast+)
   40.14  done
   40.15  
   40.16 -lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   40.17 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
   40.18  
   40.19 -lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   40.20 +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
   40.21  
   40.22  
   40.23  lemma parts_analz [simp]: "parts (analz H) = parts H"
   40.24 @@ -440,7 +440,7 @@
   40.25  apply (erule analz.induct, auto)
   40.26  done
   40.27  
   40.28 -lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   40.29 +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
   40.30  
   40.31  subsubsection{*General equational properties*}
   40.32  
   40.33 @@ -811,7 +811,7 @@
   40.34  text{*Rewrites to push in Key and Crypt messages, so that other messages can
   40.35      be pulled out using the @{text analz_insert} rules*}
   40.36  
   40.37 -lemmas pushKeys [standard] =
   40.38 +lemmas pushKeys =
   40.39    insert_commute [of "Key K" "Agent C"]
   40.40    insert_commute [of "Key K" "Nonce N"]
   40.41    insert_commute [of "Key K" "Number N"]
   40.42 @@ -819,14 +819,16 @@
   40.43    insert_commute [of "Key K" "Hash X"]
   40.44    insert_commute [of "Key K" "MPair X Y"]
   40.45    insert_commute [of "Key K" "Crypt X K'"]
   40.46 +  for K C N PAN X Y K'
   40.47  
   40.48 -lemmas pushCrypts [standard] =
   40.49 +lemmas pushCrypts =
   40.50    insert_commute [of "Crypt X K" "Agent C"]
   40.51    insert_commute [of "Crypt X K" "Nonce N"]
   40.52    insert_commute [of "Crypt X K" "Number N"]
   40.53    insert_commute [of "Crypt X K" "Pan PAN"]
   40.54    insert_commute [of "Crypt X K" "Hash X'"]
   40.55    insert_commute [of "Crypt X K" "MPair X' Y"]
   40.56 +  for X K C N PAN X' Y
   40.57  
   40.58  text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   40.59    re-ordered.*}
    41.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 20 20:59:30 2011 +0100
    41.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 20 21:05:23 2011 +0100
    41.3 @@ -819,7 +819,7 @@
    41.4    apply force
    41.5    done
    41.6  (* turn into (unsafe, looping!) introduction rule *)
    41.7 -lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard]
    41.8 +lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
    41.9  
   41.10  lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   41.11           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
    42.1 --- a/src/HOL/TLA/TLA.thy	Sun Nov 20 20:59:30 2011 +0100
    42.2 +++ b/src/HOL/TLA/TLA.thy	Sun Nov 20 21:05:23 2011 +0100
    42.3 @@ -149,7 +149,7 @@
    42.4  section "Simple temporal logic"
    42.5  
    42.6  (* []~F == []~Init F *)
    42.7 -lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps, standard]
    42.8 +lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F
    42.9  
   42.10  lemma dmdInit: "TEMP <>F == TEMP <> Init F"
   42.11    apply (unfold dmd_def)
   42.12 @@ -157,15 +157,15 @@
   42.13    apply (simp (no_asm) add: Init_simps)
   42.14    done
   42.15  
   42.16 -lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps, standard]
   42.17 +lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F
   42.18  
   42.19  (* boxInit and dmdInit cannot be used as rewrites, because they loop.
   42.20     Non-looping instances for state predicates and actions are occasionally useful.
   42.21  *)
   42.22 -lemmas boxInit_stp = boxInit [where 'a = state, standard]
   42.23 -lemmas boxInit_act = boxInit [where 'a = "state * state", standard]
   42.24 -lemmas dmdInit_stp = dmdInit [where 'a = state, standard]
   42.25 -lemmas dmdInit_act = dmdInit [where 'a = "state * state", standard]
   42.26 +lemmas boxInit_stp = boxInit [where 'a = state]
   42.27 +lemmas boxInit_act = boxInit [where 'a = "state * state"]
   42.28 +lemmas dmdInit_stp = dmdInit [where 'a = state]
   42.29 +lemmas dmdInit_act = dmdInit [where 'a = "state * state"]
   42.30  
   42.31  (* The symmetric equations can be used to get rid of Init *)
   42.32  lemmas boxInitD = boxInit [symmetric]
   42.33 @@ -208,14 +208,14 @@
   42.34     [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
   42.35  *)
   42.36  lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
   42.37 -lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1, standard]
   42.38 +lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
   42.39  
   42.40  (* dual versions for <> *)
   42.41  lemma DmdDmd: "|- (<><>F) = (<>F)"
   42.42    by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
   42.43  
   42.44  lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
   42.45 -lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1, standard]
   42.46 +lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1]
   42.47  
   42.48  
   42.49  (* ------------------------ STL4 ------------------------------------------- *)
   42.50 @@ -266,7 +266,7 @@
   42.51    done
   42.52  
   42.53  (* rewrite rule to split conjunctions under boxes *)
   42.54 -lemmas split_box_conj = STL5 [temp_unlift, symmetric, standard]
   42.55 +lemmas split_box_conj = STL5 [temp_unlift, symmetric]
   42.56  
   42.57  
   42.58  (* the corresponding elimination rule allows to combine boxes in the hypotheses
   42.59 @@ -283,9 +283,9 @@
   42.60  (* Instances of box_conjE for state predicates, actions, and temporals
   42.61     in case the general rule is "too polymorphic".
   42.62  *)
   42.63 -lemmas box_conjE_temp = box_conjE [where 'a = behavior, standard]
   42.64 -lemmas box_conjE_stp = box_conjE [where 'a = state, standard]
   42.65 -lemmas box_conjE_act = box_conjE [where 'a = "state * state", standard]
   42.66 +lemmas box_conjE_temp = box_conjE [where 'a = behavior]
   42.67 +lemmas box_conjE_stp = box_conjE [where 'a = state]
   42.68 +lemmas box_conjE_act = box_conjE [where 'a = "state * state"]
   42.69  
   42.70  (* Define a tactic that tries to merge all boxes in an antecedent. The definition is
   42.71     a bit kludgy in order to simulate "double elim-resolution".
   42.72 @@ -318,7 +318,7 @@
   42.73  (* rewrite rule to push universal quantification through box:
   42.74        (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
   42.75  *)
   42.76 -lemmas all_box = allT [temp_unlift, symmetric, standard]
   42.77 +lemmas all_box = allT [temp_unlift, symmetric]
   42.78  
   42.79  lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
   42.80    apply (auto simp add: dmd_def split_box_conj [try_rewrite])
   42.81 @@ -328,7 +328,7 @@
   42.82  lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
   42.83    by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
   42.84  
   42.85 -lemmas ex_dmd = exT [temp_unlift, symmetric, standard]
   42.86 +lemmas ex_dmd = exT [temp_unlift, symmetric]
   42.87  
   42.88  lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
   42.89    apply (erule dup_boxE)
   42.90 @@ -526,7 +526,7 @@
   42.91    apply (fastforce elim!: TLA2E [temp_use])
   42.92    done
   42.93  
   42.94 -lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use], standard]
   42.95 +lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]]
   42.96  
   42.97  (* ------------------------ INV1, stable --------------------------------------- *)
   42.98  section "stable, invariant"
   42.99 @@ -541,8 +541,8 @@
  42.100  lemma box_stp_act: "|- ([]$P) = ([]P)"
  42.101    by (simp add: boxInit_act Init_simps)
  42.102  
  42.103 -lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2, standard]
  42.104 -lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1, standard]
  42.105 +lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
  42.106 +lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1]
  42.107  
  42.108  lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
  42.109  
  42.110 @@ -710,7 +710,7 @@
  42.111    done
  42.112  
  42.113  (* |- F & (F ~> G) --> <>G *)
  42.114 -lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps, standard]
  42.115 +lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
  42.116  
  42.117  lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))"
  42.118    apply (unfold leadsto_def)
  42.119 @@ -776,8 +776,8 @@
  42.120      elim!: STL4E_gen [temp_use] simp: Init_simps)
  42.121    done
  42.122  
  42.123 -lemmas ImplLeadsto = ImplLeadsto_gen [where 'a = behavior and 'b = behavior,
  42.124 -  unfolded Init_simps, standard]
  42.125 +lemmas ImplLeadsto =
  42.126 +  ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
  42.127  
  42.128  lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G"
  42.129    by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
  42.130 @@ -1065,7 +1065,7 @@
  42.131  
  42.132  (* "wf r  ==>  |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *)
  42.133  lemmas wf_not_dmd_box_decrease =
  42.134 -  wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps, standard]
  42.135 +  wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
  42.136  
  42.137  (* If there are infinitely many steps where v decreases, then there
  42.138     have to be infinitely many non-stuttering steps where v doesn't decrease.
    43.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 20 20:59:30 2011 +0100
    43.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 20 21:05:23 2011 +0100
    43.3 @@ -791,7 +791,7 @@
    43.4    done
    43.5  
    43.6  lemmas rename_guarantees_sysOfAlloc_I =
    43.7 -  bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2, standard]
    43.8 +  bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2]
    43.9  
   43.10  
   43.11  (*Lifting Alloc_Increasing up to the level of systemState*)
   43.12 @@ -867,7 +867,7 @@
   43.13  
   43.14  text{*safety (1), step 2*}
   43.15  (* i < Nclients ==> System : Increasing (sub i o allocRel) *)
   43.16 -lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard]
   43.17 +lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1]
   43.18  
   43.19  (*Lifting Alloc_safety up to the level of systemState.
   43.20    Simplifying with o_def gets rid of the translations but it unfortunately
   43.21 @@ -921,7 +921,7 @@
   43.22  
   43.23  text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
   43.24  (* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
   43.25 -lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1, standard]
   43.26 +lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1]
   43.27  
   43.28  text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
   43.29  lemma rename_Client_Bounded: "i : I
   43.30 @@ -955,7 +955,7 @@
   43.31  
   43.32  text{*progress (2), step 6*}
   43.33  (* i < Nclients ==> System : Increasing (giv o sub i o client) *)
   43.34 -lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1, standard]
   43.35 +lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1]
   43.36  
   43.37  
   43.38  lemma rename_Client_Progress: "i: I
    44.1 --- a/src/HOL/UNITY/Constrains.thy	Sun Nov 20 20:59:30 2011 +0100
    44.2 +++ b/src/HOL/UNITY/Constrains.thy	Sun Nov 20 21:05:23 2011 +0100
    44.3 @@ -86,8 +86,7 @@
    44.4  
    44.5  (*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
    44.6  lemmas constrains_reachable_Int =  
    44.7 -    subset_refl [THEN stable_reachable [unfolded stable_def], 
    44.8 -                 THEN constrains_Int, standard]
    44.9 +    subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]
   44.10  
   44.11  (*Resembles the previous definition of Constrains*)
   44.12  lemma Constrains_eq_constrains: 
   44.13 @@ -263,8 +262,7 @@
   44.14  apply (blast intro: stable_imp_Stable)
   44.15  done
   44.16  
   44.17 -lemmas Increasing_constant =  
   44.18 -    increasing_constant [THEN increasing_imp_Increasing, standard, iff]
   44.19 +lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
   44.20  
   44.21  
   44.22  subsection{*The Elimination Theorem*}
   44.23 @@ -294,8 +292,8 @@
   44.24  lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
   44.25  by (simp add: Always_def)
   44.26  
   44.27 -lemmas AlwaysE = AlwaysD [THEN conjE, standard]
   44.28 -lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
   44.29 +lemmas AlwaysE = AlwaysD [THEN conjE]
   44.30 +lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
   44.31  
   44.32  
   44.33  (*The set of all reachable states is Always*)
   44.34 @@ -312,8 +310,7 @@
   44.35  apply (blast intro: constrains_imp_Constrains)
   44.36  done
   44.37  
   44.38 -lemmas Always_reachable =
   44.39 -    invariant_reachable [THEN invariant_imp_Always, standard]
   44.40 +lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
   44.41  
   44.42  lemma Always_eq_invariant_reachable:
   44.43       "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
   44.44 @@ -355,10 +352,10 @@
   44.45                Constrains_eq_constrains Int_assoc [symmetric])
   44.46  
   44.47  (* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
   44.48 -lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
   44.49 +lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1]
   44.50  
   44.51  (* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
   44.52 -lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
   44.53 +lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
   44.54  
   44.55  (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
   44.56  lemma Always_Constrains_weaken:
   44.57 @@ -390,7 +387,7 @@
   44.58  
   44.59  (*Delete the nearest invariance assumption (which will be the second one
   44.60    used by Always_Int_I) *)
   44.61 -lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
   44.62 +lemmas Always_thin = thin_rl [of "F \<in> Always A"]
   44.63  
   44.64  
   44.65  subsection{*Totalize*}
    45.1 --- a/src/HOL/UNITY/ELT.thy	Sun Nov 20 20:59:30 2011 +0100
    45.2 +++ b/src/HOL/UNITY/ELT.thy	Sun Nov 20 21:05:23 2011 +0100
    45.3 @@ -418,7 +418,7 @@
    45.4  apply (blast intro: subset_imp_leadsETo)
    45.5  done
    45.6  
    45.7 -lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
    45.8 +lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
    45.9  
   45.10  lemma LeadsETo_weaken_R [rule_format]:
   45.11       "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
    46.1 --- a/src/HOL/UNITY/Rename.thy	Sun Nov 20 20:59:30 2011 +0100
    46.2 +++ b/src/HOL/UNITY/Rename.thy	Sun Nov 20 21:05:23 2011 +0100
    46.3 @@ -140,7 +140,7 @@
    46.4  lemma bij_rename: "bij h ==> bij (rename h)"
    46.5  apply (simp (no_asm_simp) add: rename_def bij_extend)
    46.6  done
    46.7 -lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
    46.8 +lemmas surj_rename = bij_rename [THEN bij_is_surj]
    46.9  
   46.10  lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
   46.11  apply (unfold inj_on_def, auto)
    47.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Sun Nov 20 20:59:30 2011 +0100
    47.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Sun Nov 20 21:05:23 2011 +0100
    47.3 @@ -69,8 +69,8 @@
    47.4      MA7:  "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
    47.5  
    47.6  
    47.7 -lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard]
    47.8 -lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard]
    47.9 +lemmas E_imp_in_V_L = Graph2 [THEN conjunct1]
   47.10 +lemmas E_imp_in_V_R = Graph2 [THEN conjunct2]
   47.11  
   47.12  lemma lemma2:
   47.13       "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
    48.1 --- a/src/HOL/UNITY/SubstAx.thy	Sun Nov 20 20:59:30 2011 +0100
    48.2 +++ b/src/HOL/UNITY/SubstAx.thy	Sun Nov 20 21:05:23 2011 +0100
    48.3 @@ -42,10 +42,10 @@
    48.4                Int_assoc [symmetric])
    48.5  
    48.6  (* [| F \<in> Always C;  F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
    48.7 -lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
    48.8 +lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1]
    48.9  
   48.10  (* [| F \<in> Always INV;  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
   48.11 -lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
   48.12 +lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2]
   48.13  
   48.14  
   48.15  subsection{*Introduction rules: Basis, Trans, Union*}
   48.16 @@ -104,7 +104,7 @@
   48.17  apply (blast intro: subset_imp_leadsTo)
   48.18  done
   48.19  
   48.20 -lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
   48.21 +lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, simp]
   48.22  
   48.23  lemma LeadsTo_weaken_R:
   48.24       "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
    49.1 --- a/src/HOL/UNITY/UNITY.thy	Sun Nov 20 20:59:30 2011 +0100
    49.2 +++ b/src/HOL/UNITY/UNITY.thy	Sun Nov 20 21:05:23 2011 +0100
    49.3 @@ -274,7 +274,7 @@
    49.4  by (unfold stable_def constrains_def, blast)
    49.5  
    49.6  (*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
    49.7 -lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
    49.8 +lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
    49.9  
   49.10  
   49.11  subsubsection{*invariant*}
    50.1 --- a/src/HOL/UNITY/Union.thy	Sun Nov 20 20:59:30 2011 +0100
    50.2 +++ b/src/HOL/UNITY/Union.thy	Sun Nov 20 21:05:23 2011 +0100
    50.3 @@ -332,7 +332,7 @@
    50.4  lemma ok_commute: "(F ok G) = (G ok F)"
    50.5  by (auto simp add: ok_def)
    50.6  
    50.7 -lemmas ok_sym = ok_commute [THEN iffD1, standard]
    50.8 +lemmas ok_sym = ok_commute [THEN iffD1]
    50.9  
   50.10  lemma ok_iff_OK:
   50.11       "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
    51.1 --- a/src/HOL/UNITY/WFair.thy	Sun Nov 20 20:59:30 2011 +0100
    51.2 +++ b/src/HOL/UNITY/WFair.thy	Sun Nov 20 21:05:23 2011 +0100
    51.3 @@ -235,13 +235,13 @@
    51.4  lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
    51.5  by (unfold ensures_def constrains_def transient_def, blast)
    51.6  
    51.7 -lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
    51.8 +lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
    51.9  
   51.10 -lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
   51.11 +lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo]
   51.12  
   51.13 -lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
   51.14 +lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, simp]
   51.15  
   51.16 -lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
   51.17 +lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, simp]
   51.18  
   51.19  
   51.20  
    52.1 --- a/src/HOL/ex/Gauge_Integration.thy	Sun Nov 20 20:59:30 2011 +0100
    52.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Sun Nov 20 21:05:23 2011 +0100
    52.3 @@ -45,7 +45,7 @@
    52.4        \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
    52.5  
    52.6  lemmas fine_induct [induct set: fine] =
    52.7 -  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
    52.8 +  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
    52.9  
   52.10  lemma fine_single:
   52.11    "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
    53.1 --- a/src/HOL/ex/Tree23.thy	Sun Nov 20 20:59:30 2011 +0100
    53.2 +++ b/src/HOL/ex/Tree23.thy	Sun Nov 20 21:05:23 2011 +0100
    53.3 @@ -330,12 +330,13 @@
    53.4  "dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
    53.5  
    53.6  lemmas dfull_case_intros =
    53.7 -  ord.exhaust [where y=y and P="dfull a (ord_case b c d y)", standard]
    53.8 -  option.exhaust [where y=y and P="dfull a (option_case b c y)", standard]
    53.9 -  prod.exhaust [where y=y and P="dfull a (prod_case b y)", standard]
   53.10 -  bool.exhaust [where y=y and P="dfull a (bool_case b c y)", standard]
   53.11 -  tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))", standard]
   53.12 -  tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
   53.13 +  ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
   53.14 +  option.exhaust [where y=y and P="dfull a (option_case b c y)"]
   53.15 +  prod.exhaust [where y=y and P="dfull a (prod_case b y)"]
   53.16 +  bool.exhaust [where y=y and P="dfull a (bool_case b c y)"]
   53.17 +  tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]
   53.18 +  tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"]
   53.19 +  for a b c d e y
   53.20  
   53.21  lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
   53.22  proof -