eliminated obsolete "standard";
authorwenzelm
Sun Nov 20 20:15:02 2011 +0100 (2011-11-20)
changeset 456022a858377c3d2
parent 45601 d5178f19b671
child 45603 d2d9ef16ccaf
eliminated obsolete "standard";
src/FOLP/IFOLP.thy
src/Sequents/LK.thy
src/Sequents/LK0.thy
src/ZF/AC/HH.thy
src/ZF/AC/Hartog.thy
src/ZF/AC/WO2_AC16.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Coind/ECR.thy
src/ZF/Constructible/Formula.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/Induct/Multiset.thy
src/ZF/Induct/Tree_Forest.thy
src/ZF/IntArith.thy
src/ZF/IntDiv_ZF.thy
src/ZF/Int_ZF.thy
src/ZF/List_ZF.thy
src/ZF/Nat_ZF.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Resid/Confluence.thy
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/UNITY/AllocBase.thy
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/FP.thy
src/ZF/UNITY/GenPrefix.thy
src/ZF/UNITY/UNITY.thy
src/ZF/UNITY/Union.thy
src/ZF/UNITY/WFair.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.thy
src/ZF/Zorn.thy
src/ZF/equalities.thy
src/ZF/ex/Limit.thy
src/ZF/ex/Primes.thy
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/src/FOLP/IFOLP.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -504,7 +504,7 @@
     1.4  lemmas pred_congs = pred1_cong pred2_cong pred3_cong
     1.5  
     1.6  (*special case for the equality predicate!*)
     1.7 -lemmas eq_cong = pred2_cong [where P = "op =", standard]
     1.8 +lemmas eq_cong = pred2_cong [where P = "op ="]
     1.9  
    1.10  
    1.11  (*** Simplifications of assumed implications.
     2.1 --- a/src/Sequents/LK.thy	Sun Nov 20 17:57:09 2011 +0100
     2.2 +++ b/src/Sequents/LK.thy	Sun Nov 20 20:15:02 2011 +0100
     2.3 @@ -129,14 +129,14 @@
     2.4    apply (tactic {* fast_tac LK_pack 1 *})
     2.5    done
     2.6  
     2.7 -lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard]
     2.8 +lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
     2.9  
    2.10  lemma P_iff_T: "|- P ==> |- (P <-> True)"
    2.11    apply (erule thinR [THEN cut])
    2.12    apply (tactic {* fast_tac LK_pack 1 *})
    2.13    done
    2.14  
    2.15 -lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard]
    2.16 +lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
    2.17  
    2.18  
    2.19  lemma LK_extra_simps:
     3.1 --- a/src/Sequents/LK0.thy	Sun Nov 20 17:57:09 2011 +0100
     3.2 +++ b/src/Sequents/LK0.thy	Sun Nov 20 20:15:02 2011 +0100
     3.3 @@ -305,10 +305,10 @@
     3.4    by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
     3.5  
     3.6  (* Symmetry of equality in hypotheses *)
     3.7 -lemmas symL = sym [THEN L_of_imp, standard]
     3.8 +lemmas symL = sym [THEN L_of_imp]
     3.9  
    3.10  (* Symmetry of equality in hypotheses *)
    3.11 -lemmas symR = sym [THEN R_of_imp, standard]
    3.12 +lemmas symR = sym [THEN R_of_imp]
    3.13  
    3.14  lemma transR: "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
    3.15    by (rule trans [THEN R_of_imp, THEN mp_R])
     4.1 --- a/src/ZF/AC/HH.thy	Sun Nov 20 17:57:09 2011 +0100
     4.2 +++ b/src/ZF/AC/HH.thy	Sun Nov 20 20:15:02 2011 +0100
     4.3 @@ -210,7 +210,7 @@
     4.4    simplification is needed!*)
     4.5  lemmas bij_Least_HH_x =  
     4.6      comp_bij [OF f_sing_lam_bij [OF _ lam_singI] 
     4.7 -              lam_sing_bij [THEN bij_converse_bij], standard]
     4.8 +              lam_sing_bij [THEN bij_converse_bij]]
     4.9  
    4.10  
    4.11  subsection{*The proof of AC1 ==> WO2*}
     5.1 --- a/src/ZF/AC/Hartog.thy	Sun Nov 20 17:57:09 2011 +0100
     5.2 +++ b/src/ZF/AC/Hartog.thy	Sun Nov 20 20:15:02 2011 +0100
     5.3 @@ -65,7 +65,7 @@
     5.4  apply (rule LeastI, auto) 
     5.5  done
     5.6  
     5.7 -lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE, standard]
     5.8 +lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE]
     5.9  
    5.10  lemma Ord_Hartog: "Ord(Hartog(A))"
    5.11  by (unfold Hartog_def, rule Ord_Least)
     6.1 --- a/src/ZF/AC/WO2_AC16.thy	Sun Nov 20 17:57:09 2011 +0100
     6.2 +++ b/src/ZF/AC/WO2_AC16.thy	Sun Nov 20 20:15:02 2011 +0100
     6.3 @@ -315,8 +315,7 @@
     6.4  
     6.5  lemmas disj_Un_eqpoll_nat_sum = 
     6.6      eqpoll_trans [THEN eqpoll_trans, 
     6.7 -                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum,
     6.8 -                  standard];
     6.9 +                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum];
    6.10  
    6.11  
    6.12  lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;   
     7.1 --- a/src/ZF/AC/WO6_WO1.thy	Sun Nov 20 17:57:09 2011 +0100
     7.2 +++ b/src/ZF/AC/WO6_WO1.thy	Sun Nov 20 20:15:02 2011 +0100
     7.3 @@ -217,10 +217,9 @@
     7.4  apply (fast elim!: LeastI)+
     7.5  done
     7.6  
     7.7 -lemmas nested_Least_instance = 
     7.8 +lemmas nested_Least_instance =
     7.9         nested_LeastI [of "%g d. domain(uu(f,b,g,d)) \<noteq> 0 & 
    7.10 -                                domain(uu(f,b,g,d)) \<lesssim> m", 
    7.11 -                      standard]    (*generalizes the Variables!*)
    7.12 +                                domain(uu(f,b,g,d)) \<lesssim> m"] for f b m
    7.13  
    7.14  lemma gg1_lepoll_m: 
    7.15       "[| Ord(a);  m \<in> nat;   
     8.1 --- a/src/ZF/Bool.thy	Sun Nov 20 17:57:09 2011 +0100
     8.2 +++ b/src/ZF/Bool.thy	Sun Nov 20 20:15:02 2011 +0100
     8.3 @@ -53,7 +53,7 @@
     8.4  by (simp add: bool_defs )
     8.5  
     8.6  (** 1=0 ==> R **)
     8.7 -lemmas one_neq_0 = one_not_0 [THEN notE, standard]
     8.8 +lemmas one_neq_0 = one_not_0 [THEN notE]
     8.9  
    8.10  lemma boolE:
    8.11      "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"
    8.12 @@ -82,17 +82,17 @@
    8.13  lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
    8.14  by simp
    8.15  
    8.16 -lemmas not_1 = not_def [THEN def_cond_1, standard, simp]
    8.17 -lemmas not_0 = not_def [THEN def_cond_0, standard, simp]
    8.18 +lemmas not_1 = not_def [THEN def_cond_1, simp]
    8.19 +lemmas not_0 = not_def [THEN def_cond_0, simp]
    8.20  
    8.21 -lemmas and_1 = and_def [THEN def_cond_1, standard, simp]
    8.22 -lemmas and_0 = and_def [THEN def_cond_0, standard, simp]
    8.23 +lemmas and_1 = and_def [THEN def_cond_1, simp]
    8.24 +lemmas and_0 = and_def [THEN def_cond_0, simp]
    8.25  
    8.26 -lemmas or_1 = or_def [THEN def_cond_1, standard, simp]
    8.27 -lemmas or_0 = or_def [THEN def_cond_0, standard, simp]
    8.28 +lemmas or_1 = or_def [THEN def_cond_1, simp]
    8.29 +lemmas or_0 = or_def [THEN def_cond_0, simp]
    8.30  
    8.31 -lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp]
    8.32 -lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp]
    8.33 +lemmas xor_1 = xor_def [THEN def_cond_1, simp]
    8.34 +lemmas xor_0 = xor_def [THEN def_cond_0, simp]
    8.35  
    8.36  lemma not_type [TC]: "a:bool ==> not(a) : bool"
    8.37  by (simp add: not_def)
     9.1 --- a/src/ZF/Cardinal.thy	Sun Nov 20 17:57:09 2011 +0100
     9.2 +++ b/src/ZF/Cardinal.thy	Sun Nov 20 20:15:02 2011 +0100
     9.3 @@ -94,7 +94,7 @@
     9.4  done
     9.5  
     9.6  (*A eqpoll A*)
     9.7 -lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp]
     9.8 +lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
     9.9  
    9.10  lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
    9.11  apply (unfold eqpoll_def)
    9.12 @@ -115,9 +115,9 @@
    9.13  apply (erule id_subset_inj)
    9.14  done
    9.15  
    9.16 -lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp]
    9.17 +lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp]
    9.18  
    9.19 -lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard]
    9.20 +lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
    9.21  
    9.22  lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
    9.23  by (unfold eqpoll_def bij_def lepoll_def, blast)
    9.24 @@ -147,7 +147,7 @@
    9.25  done
    9.26  
    9.27  (*0 \<lesssim> Y*)
    9.28 -lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard]
    9.29 +lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
    9.30  
    9.31  lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
    9.32  by (blast intro: lepoll_0_is_0 lepoll_refl)
    9.33 @@ -159,7 +159,7 @@
    9.34  done
    9.35  
    9.36  (*A eqpoll 0 ==> A=0*)
    9.37 -lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard]
    9.38 +lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
    9.39  
    9.40  lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
    9.41  by (blast intro: eqpoll_0_is_0 eqpoll_refl)
    9.42 @@ -791,12 +791,12 @@
    9.43                                         [unfolded Finite_def]])
    9.44  done
    9.45  
    9.46 -lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard]
    9.47 +lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
    9.48  
    9.49  lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A Int B)"
    9.50  by (blast intro: subset_Finite) 
    9.51  
    9.52 -lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard]
    9.53 +lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
    9.54  
    9.55  lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
    9.56  apply (unfold Finite_def)
    10.1 --- a/src/ZF/CardinalArith.thy	Sun Nov 20 17:57:09 2011 +0100
    10.2 +++ b/src/ZF/CardinalArith.thy	Sun Nov 20 20:15:02 2011 +0100
    10.3 @@ -753,9 +753,9 @@
    10.4  apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
    10.5  done
    10.6  
    10.7 -lemmas Card_csucc = csucc_basic [THEN conjunct1, standard]
    10.8 +lemmas Card_csucc = csucc_basic [THEN conjunct1]
    10.9  
   10.10 -lemmas lt_csucc = csucc_basic [THEN conjunct2, standard]
   10.11 +lemmas lt_csucc = csucc_basic [THEN conjunct2]
   10.12  
   10.13  lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"
   10.14  by (blast intro: Ord_0_le lt_csucc lt_trans1)
   10.15 @@ -857,7 +857,7 @@
   10.16  
   10.17  subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*}
   10.18  
   10.19 -lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard]
   10.20 +lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]
   10.21  
   10.22  lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n"
   10.23  apply (rule eqpoll_trans)
    11.1 --- a/src/ZF/Cardinal_AC.thy	Sun Nov 20 17:57:09 2011 +0100
    11.2 +++ b/src/ZF/Cardinal_AC.thy	Sun Nov 20 20:15:02 2011 +0100
    11.3 @@ -17,7 +17,7 @@
    11.4  done
    11.5  
    11.6  text{*The theorem @{term "||A|| = |A|"} *}
    11.7 -lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp]
    11.8 +lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
    11.9  
   11.10  lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
   11.11  apply (rule AC_well_ord [THEN exE])
    12.1 --- a/src/ZF/Coind/ECR.thy	Sun Nov 20 17:57:09 2011 +0100
    12.2 +++ b/src/ZF/Coind/ECR.thy	Sun Nov 20 20:15:02 2011 +0100
    12.3 @@ -52,7 +52,7 @@
    12.4  (* Properties of the pointwise extension to environments *)
    12.5  
    12.6  lemmas HasTyRel_non_zero =
    12.7 -       HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE, standard]
    12.8 +       HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]
    12.9  
   12.10  lemma hastyenv_owr: 
   12.11    "[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |] 
    13.1 --- a/src/ZF/Constructible/Formula.thy	Sun Nov 20 17:57:09 2011 +0100
    13.2 +++ b/src/ZF/Constructible/Formula.thy	Sun Nov 20 20:15:02 2011 +0100
    13.3 @@ -805,8 +805,8 @@
    13.4  apply (blast intro: doubleton_in_Lset) 
    13.5  done
    13.6  
    13.7 -lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
    13.8 -lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
    13.9 +lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD]]
   13.10 +lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD]]
   13.11  
   13.12  text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
   13.13  lemma doubleton_in_LLimit:
    14.1 --- a/src/ZF/Epsilon.thy	Sun Nov 20 17:57:09 2011 +0100
    14.2 +++ b/src/ZF/Epsilon.thy	Sun Nov 20 20:15:02 2011 +0100
    14.3 @@ -45,7 +45,7 @@
    14.4  apply (rule nat_0I [THEN UN_upper])
    14.5  done
    14.6  
    14.7 -lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard]
    14.8 +lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
    14.9  
   14.10  lemma Transset_eclose: "Transset(eclose(A))"
   14.11  apply (unfold eclose_def Transset_def)
   14.12 @@ -58,13 +58,13 @@
   14.13  
   14.14  (* x : eclose(A) ==> x <= eclose(A) *)
   14.15  lemmas eclose_subset =  
   14.16 -       Transset_eclose [unfolded Transset_def, THEN bspec, standard]
   14.17 +       Transset_eclose [unfolded Transset_def, THEN bspec]
   14.18  
   14.19  (* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
   14.20 -lemmas ecloseD = eclose_subset [THEN subsetD, standard]
   14.21 +lemmas ecloseD = eclose_subset [THEN subsetD]
   14.22  
   14.23  lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
   14.24 -lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard]
   14.25 +lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD]
   14.26  
   14.27  (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
   14.28     [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
   14.29 @@ -148,7 +148,7 @@
   14.30  by (simp add: lt_def Ord_def under_Memrel) 
   14.31  
   14.32  (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
   14.33 -lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
   14.34 +lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel]
   14.35  
   14.36  lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
   14.37  
    15.1 --- a/src/ZF/Finite.thy	Sun Nov 20 17:57:09 2011 +0100
    15.2 +++ b/src/ZF/Finite.thy	Sun Nov 20 20:15:02 2011 +0100
    15.3 @@ -48,7 +48,7 @@
    15.4  done
    15.5  
    15.6  (* A : Fin(B) ==> A <= B *)
    15.7 -lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD, standard]
    15.8 +lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD]
    15.9  
   15.10  (** Induction on finite sets **)
   15.11  
   15.12 @@ -147,7 +147,7 @@
   15.13  lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
   15.14  by (erule FiniteFun.induct, simp, simp)
   15.15  
   15.16 -lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
   15.17 +lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type]
   15.18  
   15.19  (*Every subset of a finite function is a finite function.*)
   15.20  lemma FiniteFun_subset_lemma [rule_format]:
    16.1 --- a/src/ZF/Induct/Multiset.thy	Sun Nov 20 17:57:09 2011 +0100
    16.2 +++ b/src/ZF/Induct/Multiset.thy	Sun Nov 20 20:15:02 2011 +0100
    16.3 @@ -221,7 +221,7 @@
    16.4  
    16.5  (** normalize **)
    16.6  
    16.7 -lemmas Collect_Finite = Collect_subset [THEN subset_Finite, standard]
    16.8 +lemmas Collect_Finite = Collect_subset [THEN subset_Finite]
    16.9  
   16.10  lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)"
   16.11  apply (simp add: normalize_def funrestrict_def mset_of_def)
   16.12 @@ -1136,7 +1136,7 @@
   16.13  subsection{*Ordinal Multisets*}
   16.14  
   16.15  (* A \<subseteq> B ==>  field(Memrel(A)) \<subseteq> field(Memrel(B)) *)
   16.16 -lemmas field_Memrel_mono = Memrel_mono [THEN field_mono, standard]
   16.17 +lemmas field_Memrel_mono = Memrel_mono [THEN field_mono]
   16.18  
   16.19  (*
   16.20  [| Aa \<subseteq> Ba; A \<subseteq> B |] ==>
   16.21 @@ -1187,7 +1187,7 @@
   16.22    part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i)))
   16.23  *)
   16.24  
   16.25 -lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel, standard]
   16.26 +lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel]
   16.27  
   16.28  (*irreflexivity*)
   16.29  
   16.30 @@ -1199,7 +1199,7 @@
   16.31  done
   16.32  
   16.33  (* N<N ==> R *)
   16.34 -lemmas mless_irrefl = mless_not_refl [THEN notE, standard, elim!]
   16.35 +lemmas mless_irrefl = mless_not_refl [THEN notE, elim!]
   16.36  
   16.37  (*transitivity*)
   16.38  lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
    17.1 --- a/src/ZF/Induct/Tree_Forest.thy	Sun Nov 20 17:57:09 2011 +0100
    17.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Sun Nov 20 20:15:02 2011 +0100
    17.3 @@ -19,9 +19,10 @@
    17.4  
    17.5  (* FIXME *)
    17.6  lemmas tree'induct =
    17.7 -    tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1]
    17.8 +    tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1]
    17.9    and forest'induct =
   17.10 -    tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1]
   17.11 +    tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1]
   17.12 +  for t
   17.13  
   17.14  declare tree_forest.intros [simp, TC]
   17.15  
    18.1 --- a/src/ZF/IntArith.thy	Sun Nov 20 17:57:09 2011 +0100
    18.2 +++ b/src/ZF/IntArith.thy	Sun Nov 20 20:15:02 2011 +0100
    18.3 @@ -9,19 +9,22 @@
    18.4  **)
    18.5  
    18.6  lemmas [simp] =
    18.7 -  zminus_equation [where y = "integ_of(w)", standard]
    18.8 -  equation_zminus [where x = "integ_of(w)", standard]
    18.9 +  zminus_equation [where y = "integ_of(w)"]
   18.10 +  equation_zminus [where x = "integ_of(w)"]
   18.11 +  for w
   18.12  
   18.13  lemmas [iff] =
   18.14 -  zminus_zless [where y = "integ_of(w)", standard]
   18.15 -  zless_zminus [where x = "integ_of(w)", standard]
   18.16 +  zminus_zless [where y = "integ_of(w)"]
   18.17 +  zless_zminus [where x = "integ_of(w)"]
   18.18 +  for w
   18.19  
   18.20  lemmas [iff] =
   18.21 -  zminus_zle [where y = "integ_of(w)", standard]
   18.22 -  zle_zminus [where x = "integ_of(w)", standard]
   18.23 +  zminus_zle [where y = "integ_of(w)"]
   18.24 +  zle_zminus [where x = "integ_of(w)"]
   18.25 +  for w
   18.26  
   18.27  lemmas [simp] =
   18.28 -  Let_def [where s = "integ_of(w)", standard]
   18.29 +  Let_def [where s = "integ_of(w)"] for w
   18.30  
   18.31  
   18.32  (*** Simprocs for numeric literals ***)
   18.33 @@ -47,12 +50,13 @@
   18.34  (** For cancel_numerals **)
   18.35  
   18.36  lemmas rel_iff_rel_0_rls =
   18.37 -  zless_iff_zdiff_zless_0 [where y = "u $+ v", standard]
   18.38 -  eq_iff_zdiff_eq_0 [where y = "u $+ v", standard]
   18.39 -  zle_iff_zdiff_zle_0 [where y = "u $+ v", standard]
   18.40 +  zless_iff_zdiff_zless_0 [where y = "u $+ v"]
   18.41 +  eq_iff_zdiff_eq_0 [where y = "u $+ v"]
   18.42 +  zle_iff_zdiff_zle_0 [where y = "u $+ v"]
   18.43    zless_iff_zdiff_zless_0 [where y = n]
   18.44    eq_iff_zdiff_eq_0 [where y = n]
   18.45    zle_iff_zdiff_zle_0 [where y = n]
   18.46 +  for u v (* FIXME n (!?) *)
   18.47  
   18.48  lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
   18.49    apply (simp add: zdiff_def zadd_zmult_distrib)
    19.1 --- a/src/ZF/IntDiv_ZF.thy	Sun Nov 20 17:57:09 2011 +0100
    19.2 +++ b/src/ZF/IntDiv_ZF.thy	Sun Nov 20 20:15:02 2011 +0100
    19.3 @@ -791,8 +791,8 @@
    19.4  apply (blast dest: zle_zless_trans)+
    19.5  done
    19.6  
    19.7 -lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard]
    19.8 -and    pos_mod_bound = pos_mod [THEN conjunct2, standard]
    19.9 +lemmas pos_mod_sign = pos_mod [THEN conjunct1]
   19.10 +  and pos_mod_bound = pos_mod [THEN conjunct2]
   19.11  
   19.12  lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
   19.13  apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
   19.14 @@ -801,8 +801,8 @@
   19.15  apply (blast dest: zless_trans)+
   19.16  done
   19.17  
   19.18 -lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard]
   19.19 -and    neg_mod_bound = neg_mod [THEN conjunct2, standard]
   19.20 +lemmas neg_mod_sign = neg_mod [THEN conjunct1]
   19.21 +  and neg_mod_bound = neg_mod [THEN conjunct2]
   19.22  
   19.23  
   19.24  (** proving general properties of zdiv and zmod **)
   19.25 @@ -1111,16 +1111,16 @@
   19.26  apply (blast dest!: zle_zless_trans)+
   19.27  done
   19.28  
   19.29 -declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.30 -declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.31 -declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.32 -declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.33 -declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.34 -declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.35 -declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.36 -declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
   19.37 -declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
   19.38 -declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
   19.39 +declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.40 +declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.41 +declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.42 +declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.43 +declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.44 +declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.45 +declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.46 +declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
   19.47 +declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
   19.48 +declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
   19.49  
   19.50  
   19.51  (** Special-case simplification **)
    20.1 --- a/src/ZF/Int_ZF.thy	Sun Nov 20 17:57:09 2011 +0100
    20.2 +++ b/src/ZF/Int_ZF.thy	Sun Nov 20 20:15:02 2011 +0100
    20.3 @@ -717,7 +717,7 @@
    20.4  by (blast dest: zless_trans)
    20.5  
    20.6  (* [| z $< w; ~ P ==> w $< z |] ==> P *)
    20.7 -lemmas zless_asym = zless_not_sym [THEN swap, standard]
    20.8 +lemmas zless_asym = zless_not_sym [THEN swap]
    20.9  
   20.10  lemma zless_imp_zle: "z $< w ==> z $<= w"
   20.11  by (simp add: zle_def)
   20.12 @@ -867,16 +867,16 @@
   20.13  
   20.14  
   20.15  (*"v $<= w ==> v$+z $<= w$+z"*)
   20.16 -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
   20.17 +lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2]
   20.18  
   20.19  (*"v $<= w ==> z$+v $<= z$+w"*)
   20.20 -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
   20.21 +lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2]
   20.22  
   20.23  (*"v $<= w ==> v$+z $<= w$+z"*)
   20.24 -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
   20.25 +lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2]
   20.26  
   20.27  (*"v $<= w ==> z$+v $<= z$+w"*)
   20.28 -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
   20.29 +lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2]
   20.30  
   20.31  lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z"
   20.32  by (erule zadd_zle_mono1 [THEN zle_trans], simp)
    21.1 --- a/src/ZF/List_ZF.thy	Sun Nov 20 17:57:09 2011 +0100
    21.2 +++ b/src/ZF/List_ZF.thy	Sun Nov 20 20:15:02 2011 +0100
    21.3 @@ -317,7 +317,7 @@
    21.4  (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
    21.5  
    21.6  (* c : list(Collect(B,P)) ==> c : list(B) *)
    21.7 -lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard]
    21.8 +lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD]
    21.9  
   21.10  lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
   21.11  apply (induct_tac "l")
    22.1 --- a/src/ZF/Nat_ZF.thy	Sun Nov 20 17:57:09 2011 +0100
    22.2 +++ b/src/ZF/Nat_ZF.thy	Sun Nov 20 20:15:02 2011 +0100
    22.3 @@ -57,7 +57,7 @@
    22.4  done
    22.5  
    22.6  (* nat = {0} Un {succ(x). x:nat} *)
    22.7 -lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard]
    22.8 +lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold]]
    22.9  
   22.10  (** Type checking of 0 and successor **)
   22.11  
   22.12 @@ -80,7 +80,7 @@
   22.13  lemma bool_subset_nat: "bool <= nat"
   22.14  by (blast elim!: boolE)
   22.15  
   22.16 -lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard]
   22.17 +lemmas bool_into_nat = bool_subset_nat [THEN subsetD]
   22.18  
   22.19  
   22.20  subsection{*Injectivity Properties and Induction*}
   22.21 @@ -98,10 +98,10 @@
   22.22  by (erule nat_induct, auto)
   22.23  
   22.24  (* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
   22.25 -lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard]
   22.26 +lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le]
   22.27  
   22.28  (* i: nat ==> i le i; same thing as i<succ(i)  *)
   22.29 -lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard]
   22.30 +lemmas nat_le_refl = nat_into_Ord [THEN le_refl]
   22.31  
   22.32  lemma Ord_nat [iff]: "Ord(nat)"
   22.33  apply (rule OrdI)
    23.1 --- a/src/ZF/Perm.thy	Sun Nov 20 17:57:09 2011 +0100
    23.2 +++ b/src/ZF/Perm.thy	Sun Nov 20 20:15:02 2011 +0100
    23.3 @@ -125,7 +125,7 @@
    23.4  done
    23.5  
    23.6  text{* f: bij(A,B) ==> f: A->B *}
    23.7 -lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard]
    23.8 +lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
    23.9  
   23.10  lemma lam_bijective: 
   23.11      "[| !!x. x:A ==> c(x): B;            
   23.12 @@ -174,7 +174,7 @@
   23.13  apply (blast intro: lam_type) 
   23.14  done
   23.15  
   23.16 -lemmas id_inj = subset_refl [THEN id_subset_inj, standard]
   23.17 +lemmas id_inj = subset_refl [THEN id_subset_inj]
   23.18  
   23.19  lemma id_surj: "id(A): surj(A,A)"
   23.20  apply (unfold id_def surj_def)
   23.21 @@ -220,7 +220,7 @@
   23.22       "[|f \<in> inj(A,B); f ` x = y; x \<in> A|] ==> converse(f) ` y = x"
   23.23  by auto
   23.24  
   23.25 -lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard]
   23.26 +lemmas left_inverse_bij = bij_is_inj [THEN left_inverse]
   23.27  
   23.28  lemma right_inverse_lemma:
   23.29       "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b"
    24.1 --- a/src/ZF/QPair.thy	Sun Nov 20 17:57:09 2011 +0100
    24.2 +++ b/src/ZF/QPair.thy	Sun Nov 20 20:15:02 2011 +0100
    24.3 @@ -82,7 +82,7 @@
    24.4  apply (rule sum_equal_iff)
    24.5  done
    24.6  
    24.7 -lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
    24.8 +lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!]
    24.9  
   24.10  lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
   24.11  by blast
   24.12 @@ -249,8 +249,8 @@
   24.13  
   24.14  (*Injection and freeness rules*)
   24.15  
   24.16 -lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
   24.17 -lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
   24.18 +lemmas QInl_inject = QInl_iff [THEN iffD1]
   24.19 +lemmas QInr_inject = QInr_iff [THEN iffD1]
   24.20  lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
   24.21  lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
   24.22  
    25.1 --- a/src/ZF/QUniv.thy	Sun Nov 20 17:57:09 2011 +0100
    25.2 +++ b/src/ZF/QUniv.thy	Sun Nov 20 20:15:02 2011 +0100
    25.3 @@ -64,7 +64,7 @@
    25.4  apply (rule univ_eclose_subset_quniv)
    25.5  done
    25.6  
    25.7 -lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
    25.8 +lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD]
    25.9  
   25.10  lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
   25.11  apply (unfold quniv_def)
   25.12 @@ -72,15 +72,15 @@
   25.13  done
   25.14  
   25.15  lemmas univ_subset_into_quniv =
   25.16 -    PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
   25.17 +    PowI [THEN Pow_univ_subset_quniv [THEN subsetD]]
   25.18  
   25.19 -lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
   25.20 -lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
   25.21 -lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
   25.22 +lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv]
   25.23 +lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv]
   25.24 +lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv]
   25.25  
   25.26  lemmas A_subset_quniv =  subset_trans [OF A_subset_univ univ_subset_quniv]
   25.27  
   25.28 -lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
   25.29 +lemmas A_into_quniv = A_subset_quniv [THEN subsetD]
   25.30  
   25.31  (*** univ(A) closure for Quine-inspired pairs and injections ***)
   25.32  
   25.33 @@ -97,7 +97,7 @@
   25.34  done
   25.35  
   25.36  lemmas naturals_subset_nat = 
   25.37 -    Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
   25.38 +    Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec]
   25.39  
   25.40  lemmas naturals_subset_univ =
   25.41      subset_trans [OF naturals_subset_nat nat_subset_univ]
   25.42 @@ -128,7 +128,7 @@
   25.43  apply (erule PowD, blast) 
   25.44  done
   25.45  
   25.46 -lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
   25.47 +lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE]
   25.48  
   25.49  lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
   25.50  by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
   25.51 @@ -153,11 +153,11 @@
   25.52  lemmas nat_subset_quniv =  subset_trans [OF nat_subset_univ univ_subset_quniv]
   25.53  
   25.54  (* n:nat ==> n:quniv(A) *)
   25.55 -lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
   25.56 +lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD]
   25.57  
   25.58  lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
   25.59  
   25.60 -lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
   25.61 +lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD]
   25.62  
   25.63  
   25.64  (*Intersecting <a;b> with Vfrom...*)
    26.1 --- a/src/ZF/Resid/Confluence.thy	Sun Nov 20 17:57:09 2011 +0100
    26.2 +++ b/src/ZF/Resid/Confluence.thy	Sun Nov 20 20:15:02 2011 +0100
    26.3 @@ -52,13 +52,13 @@
    26.4  done
    26.5  
    26.6  lemmas confluence_parallel_reduction =
    26.7 -      parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
    26.8 +      parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l]
    26.9  
   26.10  lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
   26.11  by (unfold confluence_def, blast intro: par_red_red red_par_red)
   26.12  
   26.13  lemmas confluence_beta_reduction =
   26.14 -       confluence_parallel_reduction [THEN lemma1, standard]
   26.15 +       confluence_parallel_reduction [THEN lemma1]
   26.16  
   26.17  
   26.18  (**** Conversion ****)
    27.1 --- a/src/ZF/Sum.thy	Sun Nov 20 17:57:09 2011 +0100
    27.2 +++ b/src/ZF/Sum.thy	Sun Nov 20 20:15:02 2011 +0100
    27.3 @@ -94,8 +94,8 @@
    27.4  
    27.5  (*Injection and freeness rules*)
    27.6  
    27.7 -lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
    27.8 -lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
    27.9 +lemmas Inl_inject = Inl_iff [THEN iffD1]
   27.10 +lemmas Inr_inject = Inr_iff [THEN iffD1]
   27.11  lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
   27.12  lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
   27.13  
   27.14 @@ -168,7 +168,7 @@
   27.15  by blast
   27.16  
   27.17  lemmas Part_CollectE =
   27.18 -     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard]
   27.19 +     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE]
   27.20  
   27.21  lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
   27.22  by blast
    28.1 --- a/src/ZF/Trancl.thy	Sun Nov 20 17:57:09 2011 +0100
    28.2 +++ b/src/ZF/Trancl.thy	Sun Nov 20 20:15:02 2011 +0100
    28.3 @@ -109,12 +109,12 @@
    28.4  
    28.5  (* r^* = id(field(r)) Un ( r O r^* )    *)
    28.6  lemmas rtrancl_unfold =
    28.7 -     rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard]
    28.8 +     rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold]]
    28.9  
   28.10  (** The relation rtrancl **)
   28.11  
   28.12  (*  r^* <= field(r) * field(r)  *)
   28.13 -lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]
   28.14 +lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset]
   28.15  
   28.16  lemma relation_rtrancl: "relation(r^*)"
   28.17  apply (simp add: relation_def) 
   28.18 @@ -178,7 +178,7 @@
   28.19  apply (blast intro: rtrancl_into_rtrancl) 
   28.20  done
   28.21  
   28.22 -lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   28.23 +lemmas rtrancl_trans = trans_rtrancl [THEN transD]
   28.24  
   28.25  (*elimination of rtrancl -- by induction on a special formula*)
   28.26  lemma rtranclE:
   28.27 @@ -203,7 +203,7 @@
   28.28  
   28.29  lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]
   28.30  
   28.31 -lemmas trancl_trans = trans_trancl [THEN transD, standard]
   28.32 +lemmas trancl_trans = trans_trancl [THEN transD]
   28.33  
   28.34  (** Conversions between trancl and rtrancl **)
   28.35  
    29.1 --- a/src/ZF/UNITY/AllocBase.thy	Sun Nov 20 17:57:09 2011 +0100
    29.2 +++ b/src/ZF/UNITY/AllocBase.thy	Sun Nov 20 20:15:02 2011 +0100
    29.3 @@ -313,9 +313,9 @@
    29.4  done
    29.5  
    29.6  lemmas Increasing_state_ofD1 =  
    29.7 -      gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard]
    29.8 +      gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD]
    29.9  lemmas Increasing_state_ofD2 =  
   29.10 -      gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard]
   29.11 +      gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD]
   29.12  
   29.13  lemma Follows_state_of_eq: 
   29.14       "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =   
   29.15 @@ -324,9 +324,9 @@
   29.16  done
   29.17  
   29.18  lemmas Follows_state_ofD1 =
   29.19 -      Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard]
   29.20 +      Follows_state_of_eq [THEN equalityD1, THEN subsetD]
   29.21  lemmas Follows_state_ofD2 =
   29.22 -      Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard]
   29.23 +      Follows_state_of_eq [THEN equalityD2, THEN subsetD]
   29.24  
   29.25  lemma nat_list_inj_type: "n\<in>nat ==> nat_list_inj(n)\<in>list(nat)"
   29.26  by (induct_tac "n", auto)
   29.27 @@ -373,7 +373,7 @@
   29.28  by (simp add: Inter_Diff_var_iff)
   29.29  
   29.30  (* [| Finite(A); (\<forall>x\<in>var-A. b\<in>B(x)) |] ==> b\<in>Inter(RepFun(var-A, B)) *)
   29.31 -lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard]
   29.32 +lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2]
   29.33  
   29.34  declare Inter_var_DiffI [intro!]
   29.35  
    30.1 --- a/src/ZF/UNITY/Constrains.thy	Sun Nov 20 17:57:09 2011 +0100
    30.2 +++ b/src/ZF/UNITY/Constrains.thy	Sun Nov 20 20:15:02 2011 +0100
    30.3 @@ -347,8 +347,8 @@
    30.4  lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)"
    30.5  by (simp add: Always_def initially_def)
    30.6  
    30.7 -lemmas AlwaysE = AlwaysD [THEN conjE, standard]
    30.8 -lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
    30.9 +lemmas AlwaysE = AlwaysD [THEN conjE]
   30.10 +lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
   30.11  
   30.12  (*The set of all reachable states is Always*)
   30.13  lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) <= A"
   30.14 @@ -364,7 +364,7 @@
   30.15  apply (blast intro: constrains_imp_Constrains)
   30.16  done
   30.17  
   30.18 -lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always, standard]
   30.19 +lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
   30.20  
   30.21  lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) Int A)}"
   30.22  apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
   30.23 @@ -420,7 +420,7 @@
   30.24  by (blast intro: Always_Constrains_pre [THEN iffD1])
   30.25  
   30.26  (* [| F \<in> Always(I);  F \<in> A Co A' |] ==> F \<in> A Co (I Int A') *)
   30.27 -lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
   30.28 +lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
   30.29  
   30.30  (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
   30.31  lemma Always_Constrains_weaken: 
   30.32 @@ -451,7 +451,7 @@
   30.33  
   30.34  (*Delete the nearest invariance assumption (which will be the second one
   30.35    used by Always_Int_I) *)
   30.36 -lemmas Always_thin = thin_rl [of "F \<in> Always(A)", standard]
   30.37 +lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
   30.38  
   30.39  ML
   30.40  {*
    31.1 --- a/src/ZF/UNITY/FP.thy	Sun Nov 20 17:57:09 2011 +0100
    31.2 +++ b/src/ZF/UNITY/FP.thy	Sun Nov 20 20:15:02 2011 +0100
    31.3 @@ -45,7 +45,7 @@
    31.4      "[| \<forall>B. F \<in> stable (A Int B); st_set(A) |]  ==> A \<subseteq> FP_Orig(F)"
    31.5  by (unfold FP_Orig_def stable_def st_set_def, blast)
    31.6  
    31.7 -lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard]
    31.8 +lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2]
    31.9  
   31.10  lemma stable_FP_Int: "F \<in> program ==> F \<in> stable (FP(F) Int B)"
   31.11  apply (subgoal_tac "FP (F) Int B = (\<Union>x\<in>B. FP (F) Int {x}) ")
    32.1 --- a/src/ZF/UNITY/GenPrefix.thy	Sun Nov 20 17:57:09 2011 +0100
    32.2 +++ b/src/ZF/UNITY/GenPrefix.thy	Sun Nov 20 20:15:02 2011 +0100
    32.3 @@ -350,7 +350,7 @@
    32.4  apply (auto simp add: trans_def)
    32.5  done
    32.6  
    32.7 -lemmas prefix_trans = trans_prefix [THEN transD, standard]
    32.8 +lemmas prefix_trans = trans_prefix [THEN transD]
    32.9  
   32.10  lemma trans_on_prefix: "trans[list(A)](prefix(A))"
   32.11  apply (unfold prefix_def)
   32.12 @@ -358,7 +358,7 @@
   32.13  apply (auto simp add: trans_def)
   32.14  done
   32.15  
   32.16 -lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD, standard]
   32.17 +lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD]
   32.18  
   32.19  (* Monotonicity of "set" operator WRT prefix *)
   32.20  
    33.1 --- a/src/ZF/UNITY/UNITY.thy	Sun Nov 20 17:57:09 2011 +0100
    33.2 +++ b/src/ZF/UNITY/UNITY.thy	Sun Nov 20 20:15:02 2011 +0100
    33.3 @@ -167,7 +167,7 @@
    33.4  lemma Init_type: "Init(F)\<subseteq>state"
    33.5  by (simp add: RawInit_type Init_def)
    33.6  
    33.7 -lemmas InitD = Init_type [THEN subsetD, standard]
    33.8 +lemmas InitD = Init_type [THEN subsetD]
    33.9  
   33.10  lemma st_set_Init [iff]: "st_set(Init(F))"
   33.11  apply (unfold st_set_def)
   33.12 @@ -562,7 +562,7 @@
   33.13  by (unfold stable_def constrains_def st_set_def, blast)
   33.14  
   33.15  (* [| F \<in> stable(C); F  \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *)
   33.16 -lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
   33.17 +lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]
   33.18  
   33.19  subsection{*The Operator @{term invariant}*}
   33.20  
    34.1 --- a/src/ZF/UNITY/Union.thy	Sun Nov 20 17:57:09 2011 +0100
    34.2 +++ b/src/ZF/UNITY/Union.thy	Sun Nov 20 20:15:02 2011 +0100
    34.3 @@ -427,7 +427,7 @@
    34.4  lemma ok_commute: "(F ok G) <->(G ok F)"
    34.5  by (auto simp add: ok_def)
    34.6  
    34.7 -lemmas ok_sym = ok_commute [THEN iffD1, standard]
    34.8 +lemmas ok_sym = ok_commute [THEN iffD1]
    34.9  
   34.10  lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"
   34.11  by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
    35.1 --- a/src/ZF/UNITY/WFair.thy	Sun Nov 20 17:57:09 2011 +0100
    35.2 +++ b/src/ZF/UNITY/WFair.thy	Sun Nov 20 20:15:02 2011 +0100
    35.3 @@ -182,7 +182,7 @@
    35.4  
    35.5  (* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
    35.6  (* [| F \<in> program; A<=B;  st_set(A); st_set(B) |] ==> A leadsTo B *)
    35.7 -lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
    35.8 +lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
    35.9  
   35.10  lemma leadsTo_Trans: "[|F \<in> A leadsTo B;  F \<in> B leadsTo C |]==>F \<in> A leadsTo C"
   35.11  apply (unfold leadsTo_def)
   35.12 @@ -565,7 +565,7 @@
   35.13  done
   35.14  
   35.15  (* [| F \<in> program;  st_set(B) |] ==> F \<in> wlt(F, B) leadsTo B  *)
   35.16 -lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2], standard]
   35.17 +lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]
   35.18  
   35.19  lemma leadsTo_subset: "F \<in> A leadsTo B ==> A <= wlt(F, B)"
   35.20  apply (unfold wlt_def)
   35.21 @@ -665,7 +665,7 @@
   35.22  apply blast+
   35.23  done
   35.24  
   35.25 -lemmas completion = refl [THEN completion_aux, standard]
   35.26 +lemmas completion = refl [THEN completion_aux]
   35.27  
   35.28  lemma finite_completion_aux:
   35.29       "[| I \<in> Fin(X); F \<in> program; st_set(C) |] ==>  
    36.1 --- a/src/ZF/Univ.thy	Sun Nov 20 17:57:09 2011 +0100
    36.2 +++ b/src/ZF/Univ.thy	Sun Nov 20 20:15:02 2011 +0100
    36.3 @@ -205,9 +205,9 @@
    36.4  done
    36.5  
    36.6  lemmas Vfrom_UnI1 = 
    36.7 -    Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
    36.8 +    Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]]
    36.9  lemmas Vfrom_UnI2 = 
   36.10 -    Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
   36.11 +    Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]]
   36.12  
   36.13  text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
   36.14  lemma doubleton_in_VLimit:
   36.15 @@ -242,7 +242,7 @@
   36.16  
   36.17  subsubsection{* Closure under Disjoint Union *}
   36.18  
   36.19 -lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   36.20 +lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom]
   36.21  
   36.22  lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
   36.23  by (blast intro: nat_into_VLimit)
   36.24 @@ -409,8 +409,8 @@
   36.25  lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
   36.26  by (subst Vfrom, blast)
   36.27  
   36.28 -lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
   36.29 -lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
   36.30 +lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ]
   36.31 +lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom]
   36.32  
   36.33  subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *}
   36.34  
   36.35 @@ -579,7 +579,7 @@
   36.36  apply (rule A_subset_Vfrom)
   36.37  done
   36.38  
   36.39 -lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
   36.40 +lemmas A_into_univ = A_subset_univ [THEN subsetD]
   36.41  
   36.42  subsubsection{* Closure under Unordered and Ordered Pairs *}
   36.43  
   36.44 @@ -620,7 +620,7 @@
   36.45  done
   36.46  
   36.47  text{* n:nat ==> n:univ(A) *}
   36.48 -lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
   36.49 +lemmas nat_into_univ = nat_subset_univ [THEN subsetD]
   36.50  
   36.51  subsubsection{* Instances for 1 and 2 *}
   36.52  
   36.53 @@ -638,7 +638,7 @@
   36.54  apply (blast intro!: zero_in_univ one_in_univ)
   36.55  done
   36.56  
   36.57 -lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
   36.58 +lemmas bool_into_univ = bool_subset_univ [THEN subsetD]
   36.59  
   36.60  
   36.61  subsubsection{* Closure under Disjoint Union *}
   36.62 @@ -764,7 +764,7 @@
   36.63      assumption, fast)
   36.64  
   36.65  text{*This weaker version says a, b exist at the same level*}
   36.66 -lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
   36.67 +lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D]
   36.68  
   36.69  (** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
   36.70        implies a, b \<in> Vfrom(X,i), which is useless for induction.
    37.1 --- a/src/ZF/WF.thy	Sun Nov 20 17:57:09 2011 +0100
    37.2 +++ b/src/ZF/WF.thy	Sun Nov 20 20:15:02 2011 +0100
    37.3 @@ -164,7 +164,7 @@
    37.4  by (erule_tac a=a in wf_induct, blast)
    37.5  
    37.6  (* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
    37.7 -lemmas wf_asym = wf_not_sym [THEN swap, standard]
    37.8 +lemmas wf_asym = wf_not_sym [THEN swap]
    37.9  
   37.10  lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
   37.11  by (erule_tac a=a in wf_on_induct, assumption, blast)
   37.12 @@ -212,8 +212,8 @@
   37.13  
   37.14  text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}
   37.15  
   37.16 -lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
   37.17 -lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
   37.18 +lemmas underI = vimage_singleton_iff [THEN iffD2]
   37.19 +lemmas underD = vimage_singleton_iff [THEN iffD1]
   37.20  
   37.21  
   37.22  subsection{*The Predicate @{term is_recfun}*}
    38.1 --- a/src/ZF/ZF.thy	Sun Nov 20 17:57:09 2011 +0100
    38.2 +++ b/src/ZF/ZF.thy	Sun Nov 20 20:15:02 2011 +0100
    38.3 @@ -417,8 +417,8 @@
    38.4  lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
    38.5  by (rule equalityI, blast+)
    38.6  
    38.7 -lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1, standard]
    38.8 -lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2, standard]
    38.9 +lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
   38.10 +lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
   38.11  
   38.12  lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
   38.13  by (blast dest: equalityD1 equalityD2) 
   38.14 @@ -568,7 +568,7 @@
   38.15  apply (best dest: equalityD2)
   38.16  done
   38.17  
   38.18 -lemmas emptyE [elim!] = not_mem_empty [THEN notE, standard]
   38.19 +lemmas emptyE [elim!] = not_mem_empty [THEN notE]
   38.20  
   38.21  
   38.22  lemma empty_subsetI [simp]: "0 <= A"
    39.1 --- a/src/ZF/Zorn.thy	Sun Nov 20 17:57:09 2011 +0100
    39.2 +++ b/src/ZF/Zorn.thy	Sun Nov 20 20:15:02 2011 +0100
    39.3 @@ -77,9 +77,9 @@
    39.4  lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x"
    39.5  by (unfold increasing_def, blast)
    39.6  
    39.7 -lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
    39.8 +lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
    39.9  
   39.10 -lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
   39.11 +lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]
   39.12  
   39.13  
   39.14  text{*Structural induction on @{term "TFin(S,next)"} *}
    40.1 --- a/src/ZF/equalities.thy	Sun Nov 20 17:57:09 2011 +0100
    40.2 +++ b/src/ZF/equalities.thy	Sun Nov 20 20:15:02 2011 +0100
    40.3 @@ -81,7 +81,7 @@
    40.4  
    40.5  (*A safe special case of subset elimination, adding no new variables 
    40.6    [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
    40.7 -lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
    40.8 +lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
    40.9  
   40.10  lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
   40.11  by blast
    41.1 --- a/src/ZF/ex/Limit.thy	Sun Nov 20 17:57:09 2011 +0100
    41.2 +++ b/src/ZF/ex/Limit.thy	Sun Nov 20 20:15:02 2011 +0100
    41.3 @@ -994,9 +994,9 @@
    41.4  
    41.5  (* The following three theorems have cpo asms due to THE (uniqueness). *)
    41.6  
    41.7 -lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont, standard]
    41.8 -lemmas embRp_eq = embRp [THEN projpair_eq, standard]
    41.9 -lemmas embRp_rel = embRp [THEN projpair_rel, standard]
   41.10 +lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont]
   41.11 +lemmas embRp_eq = embRp [THEN projpair_eq]
   41.12 +lemmas embRp_rel = embRp [THEN projpair_rel]
   41.13  
   41.14  
   41.15  lemma embRp_eq_thm:
    42.1 --- a/src/ZF/ex/Primes.thy	Sun Nov 20 17:57:09 2011 +0100
    42.2 +++ b/src/ZF/ex/Primes.thy	Sun Nov 20 20:15:02 2011 +0100
    42.3 @@ -40,8 +40,8 @@
    42.4       "[|m dvd n;  !!k. [|m \<in> nat; n \<in> nat; k \<in> nat; n = m#*k|] ==> P|] ==> P"
    42.5  by (blast dest!: dvdD)
    42.6  
    42.7 -lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard]
    42.8 -lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard]
    42.9 +lemmas dvd_imp_nat1 = dvdD [THEN conjunct1]
   42.10 +lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1]
   42.11  
   42.12  
   42.13  lemma dvd_0_right [simp]: "m \<in> nat ==> m dvd 0"
   42.14 @@ -122,8 +122,8 @@
   42.15  done
   42.16  
   42.17  (* k dvd (m*k) *)
   42.18 -lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard]
   42.19 -lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard]
   42.20 +lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult]
   42.21 +lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2]
   42.22  
   42.23  lemma dvd_mod_imp_dvd_raw:
   42.24       "[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
    43.1 --- a/src/ZF/pair.thy	Sun Nov 20 17:57:09 2011 +0100
    43.2 +++ b/src/ZF/pair.thy	Sun Nov 20 20:15:02 2011 +0100
    43.3 @@ -43,17 +43,17 @@
    43.4  lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
    43.5  by (simp add: Pair_def doubleton_eq_iff, blast)
    43.6  
    43.7 -lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
    43.8 +lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
    43.9  
   43.10 -lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
   43.11 -lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
   43.12 +lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
   43.13 +lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
   43.14  
   43.15  lemma Pair_not_0: "<a,b> ~= 0"
   43.16  apply (unfold Pair_def)
   43.17  apply (blast elim: equalityE)
   43.18  done
   43.19  
   43.20 -lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
   43.21 +lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
   43.22  
   43.23  declare sym [THEN Pair_neq_0, elim!]
   43.24  
   43.25 @@ -82,8 +82,8 @@
   43.26  lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
   43.27  by simp
   43.28  
   43.29 -lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
   43.30 -lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
   43.31 +lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
   43.32 +lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
   43.33  
   43.34  (*The general elimination rule*)
   43.35  lemma SigmaE [elim!]:
    44.1 --- a/src/ZF/upair.thy	Sun Nov 20 17:57:09 2011 +0100
    44.2 +++ b/src/ZF/upair.thy	Sun Nov 20 20:15:02 2011 +0100
    44.3 @@ -130,7 +130,7 @@
    44.4  lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
    44.5  by (blast elim: equalityE)
    44.6  
    44.7 -lemmas cons_neq_0 = cons_not_0 [THEN notE, standard]
    44.8 +lemmas cons_neq_0 = cons_not_0 [THEN notE]
    44.9  
   44.10  declare cons_not_0 [THEN not_sym, simp]
   44.11  
   44.12 @@ -143,7 +143,7 @@
   44.13  lemma singletonI [intro!]: "a : {a}"
   44.14  by (rule consI1)
   44.15  
   44.16 -lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
   44.17 +lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!]
   44.18  
   44.19  
   44.20  subsection{*Descriptions*}
   44.21 @@ -228,11 +228,11 @@
   44.22          addsplits[split_if]
   44.23  **)
   44.24  
   44.25 -lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
   44.26 -lemmas split_if_eq2 = split_if [of "%x. a = x", standard]
   44.27 +lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
   44.28 +lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
   44.29  
   44.30 -lemmas split_if_mem1 = split_if [of "%x. x : b", standard]
   44.31 -lemmas split_if_mem2 = split_if [of "%x. a : x", standard]
   44.32 +lemmas split_if_mem1 = split_if [of "%x. x : b"] for b
   44.33 +lemmas split_if_mem2 = split_if [of "%x. a : x"] for x
   44.34  
   44.35  lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
   44.36  
   44.37 @@ -303,7 +303,7 @@
   44.38  lemma succ_not_0 [simp]: "succ(n) ~= 0"
   44.39  by (blast elim!: equalityE)
   44.40  
   44.41 -lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!]
   44.42 +lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!]
   44.43  
   44.44  declare succ_not_0 [THEN not_sym, simp]
   44.45  declare sym [THEN succ_neq_0, elim!]
   44.46 @@ -312,12 +312,12 @@
   44.47  lemmas succ_subsetD = succI1 [THEN [2] subsetD]
   44.48  
   44.49  (* succ(b) ~= b *)
   44.50 -lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard]
   44.51 +lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
   44.52  
   44.53  lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
   44.54  by (blast elim: mem_asym elim!: equalityE)
   44.55  
   44.56 -lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]
   44.57 +lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
   44.58  
   44.59  
   44.60  subsection{*Miniscoping of the Bounded Universal Quantifier*}