eliminated obsolete "standard";
authorwenzelm
Sun Nov 20 21:07:10 2011 +0100 (2011-11-20)
changeset 4560716b4f5774621
parent 45606 b1e1508643b1
child 45608 13b101cee425
eliminated obsolete "standard";
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Nat_Numeral.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Parity.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Datatype.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4  lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
     1.5  by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
     1.6  
     1.7 -lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
     1.8 +lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
     1.9  
    1.10  
    1.11  (*** Introduction rules for Node ***)
    1.12 @@ -155,7 +155,7 @@
    1.13           dest!: Abs_Node_inj 
    1.14           elim!: apfst_convE sym [THEN Push_neq_K0])  
    1.15  
    1.16 -lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
    1.17 +lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
    1.18  
    1.19  
    1.20  (*** Injectiveness ***)
    1.21 @@ -166,7 +166,7 @@
    1.22  apply (simp add: Atom_def)
    1.23  apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
    1.24  done
    1.25 -lemmas Atom_inject = inj_Atom [THEN injD, standard]
    1.26 +lemmas Atom_inject = inj_Atom [THEN injD]
    1.27  
    1.28  lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
    1.29  by (blast dest!: Atom_inject)
    1.30 @@ -177,7 +177,7 @@
    1.31  apply (erule Atom_inject [THEN Inl_inject])
    1.32  done
    1.33  
    1.34 -lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard]
    1.35 +lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
    1.36  
    1.37  lemma inj_Numb: "inj(Numb)"
    1.38  apply (simp add: Numb_def o_def)
    1.39 @@ -185,7 +185,7 @@
    1.40  apply (erule Atom_inject [THEN Inr_inject])
    1.41  done
    1.42  
    1.43 -lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard]
    1.44 +lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
    1.45  
    1.46  
    1.47  (** Injectiveness of Push_Node **)
    1.48 @@ -235,14 +235,14 @@
    1.49  lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
    1.50  unfolding Leaf_def o_def by (rule Scons_not_Atom)
    1.51  
    1.52 -lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
    1.53 +lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
    1.54  
    1.55  (** Scons vs Numb **)
    1.56  
    1.57  lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
    1.58  unfolding Numb_def o_def by (rule Scons_not_Atom)
    1.59  
    1.60 -lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
    1.61 +lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
    1.62  
    1.63  
    1.64  (** Leaf vs Numb **)
    1.65 @@ -250,7 +250,7 @@
    1.66  lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
    1.67  by (simp add: Leaf_def Numb_def)
    1.68  
    1.69 -lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard]
    1.70 +lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
    1.71  
    1.72  
    1.73  (*** ndepth -- the depth of a node ***)
    1.74 @@ -357,7 +357,7 @@
    1.75  lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
    1.76  unfolding In0_def In1_def One_nat_def by auto
    1.77  
    1.78 -lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
    1.79 +lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
    1.80  
    1.81  lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
    1.82  by (simp add: In0_def)
    1.83 @@ -503,7 +503,7 @@
    1.84  lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
    1.85  by blast
    1.86  
    1.87 -lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard]
    1.88 +lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
    1.89  
    1.90  (*Dependent version*)
    1.91  lemma dprod_subset_Sigma2:
    1.92 @@ -514,7 +514,7 @@
    1.93  lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
    1.94  by blast
    1.95  
    1.96 -lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
    1.97 +lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
    1.98  
    1.99  
   1.100  text {* hides popular names *}
     2.1 --- a/src/HOL/Divides.thy	Sun Nov 20 21:07:06 2011 +0100
     2.2 +++ b/src/HOL/Divides.thy	Sun Nov 20 21:07:10 2011 +0100
     2.3 @@ -1142,13 +1142,8 @@
     2.4  lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
     2.5  by (simp add: Suc3_eq_add_3)
     2.6  
     2.7 -lemmas Suc_div_eq_add3_div_number_of =
     2.8 -    Suc_div_eq_add3_div [of _ "number_of v", standard]
     2.9 -declare Suc_div_eq_add3_div_number_of [simp]
    2.10 -
    2.11 -lemmas Suc_mod_eq_add3_mod_number_of =
    2.12 -    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
    2.13 -declare Suc_mod_eq_add3_mod_number_of [simp]
    2.14 +lemmas Suc_div_eq_add3_div_number_of [simp] = Suc_div_eq_add3_div [of _ "number_of v"] for v
    2.15 +lemmas Suc_mod_eq_add3_mod_number_of [simp] = Suc_mod_eq_add3_mod [of _ "number_of v"] for v
    2.16  
    2.17  
    2.18  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
    2.19 @@ -1156,7 +1151,7 @@
    2.20  apply (simp_all add: mod_Suc)
    2.21  done
    2.22  
    2.23 -declare Suc_times_mod_eq [of "number_of w", standard, simp]
    2.24 +declare Suc_times_mod_eq [of "number_of w", simp] for w
    2.25  
    2.26  lemma [simp]: "n div k \<le> (Suc n) div k"
    2.27  by (simp add: div_le_mono) 
    2.28 @@ -1450,17 +1445,16 @@
    2.29  apply (auto simp add: divmod_int_rel_def mod_int_def)
    2.30  done
    2.31  
    2.32 -lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
    2.33 -   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
    2.34 +lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
    2.35 +   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
    2.36  
    2.37  lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
    2.38  apply (cut_tac a = a and b = b in divmod_int_correct)
    2.39  apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
    2.40  done
    2.41  
    2.42 -lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
    2.43 -   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard]
    2.44 -
    2.45 +lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
    2.46 +   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
    2.47  
    2.48  
    2.49  subsubsection{*General Properties of div and mod*}
    2.50 @@ -1728,11 +1722,8 @@
    2.51  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
    2.52    {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
    2.53  
    2.54 -lemmas posDivAlg_eqn_number_of [simp] =
    2.55 -    posDivAlg_eqn [of "number_of v" "number_of w", standard]
    2.56 -
    2.57 -lemmas negDivAlg_eqn_number_of [simp] =
    2.58 -    negDivAlg_eqn [of "number_of v" "number_of w", standard]
    2.59 +lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w"] for v w
    2.60 +lemmas negDivAlg_eqn_number_of [simp] = negDivAlg_eqn [of "number_of v" "number_of w"] for v w
    2.61  
    2.62  
    2.63  text{*Special-case simplification *}
    2.64 @@ -1749,25 +1740,12 @@
    2.65  (** The last remaining special cases for constant arithmetic:
    2.66      1 div z and 1 mod z **)
    2.67  
    2.68 -lemmas div_pos_pos_1_number_of [simp] =
    2.69 -    div_pos_pos [OF zero_less_one, of "number_of w", standard]
    2.70 -
    2.71 -lemmas div_pos_neg_1_number_of [simp] =
    2.72 -    div_pos_neg [OF zero_less_one, of "number_of w", standard]
    2.73 -
    2.74 -lemmas mod_pos_pos_1_number_of [simp] =
    2.75 -    mod_pos_pos [OF zero_less_one, of "number_of w", standard]
    2.76 -
    2.77 -lemmas mod_pos_neg_1_number_of [simp] =
    2.78 -    mod_pos_neg [OF zero_less_one, of "number_of w", standard]
    2.79 -
    2.80 -
    2.81 -lemmas posDivAlg_eqn_1_number_of [simp] =
    2.82 -    posDivAlg_eqn [of concl: 1 "number_of w", standard]
    2.83 -
    2.84 -lemmas negDivAlg_eqn_1_number_of [simp] =
    2.85 -    negDivAlg_eqn [of concl: 1 "number_of w", standard]
    2.86 -
    2.87 +lemmas div_pos_pos_1_number_of [simp] = div_pos_pos [OF zero_less_one, of "number_of w"] for w
    2.88 +lemmas div_pos_neg_1_number_of [simp] = div_pos_neg [OF zero_less_one, of "number_of w"] for w
    2.89 +lemmas mod_pos_pos_1_number_of [simp] = mod_pos_pos [OF zero_less_one, of "number_of w"] for w
    2.90 +lemmas mod_pos_neg_1_number_of [simp] = mod_pos_neg [OF zero_less_one, of "number_of w"] for w
    2.91 +lemmas posDivAlg_eqn_1_number_of [simp] = posDivAlg_eqn [of concl: 1 "number_of w"] for w
    2.92 +lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
    2.93  
    2.94  
    2.95  subsubsection{*Monotonicity in the First Argument (Dividend)*}
    2.96 @@ -2069,8 +2047,8 @@
    2.97  text {* Enable (lin)arith to deal with @{const div} and @{const mod}
    2.98    when these are applied to some constant that is of the form
    2.99    @{term "number_of k"}: *}
   2.100 -declare split_zdiv [of _ _ "number_of k", standard, arith_split]
   2.101 -declare split_zmod [of _ _ "number_of k", standard, arith_split]
   2.102 +declare split_zdiv [of _ _ "number_of k", arith_split] for k
   2.103 +declare split_zmod [of _ _ "number_of k", arith_split] for k
   2.104  
   2.105  
   2.106  subsubsection{*Speeding up the Division Algorithm with Shifting*}
   2.107 @@ -2257,7 +2235,7 @@
   2.108  subsubsection {* The Divides Relation *}
   2.109  
   2.110  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   2.111 -  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
   2.112 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y :: int
   2.113  
   2.114  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   2.115    by (rule dvd_mod) (* TODO: remove *)
   2.116 @@ -2456,10 +2434,8 @@
   2.117           else nat (1 mod number_of v'))"
   2.118  by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   2.119  
   2.120 -lemmas dvd_eq_mod_eq_0_number_of =
   2.121 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
   2.122 -
   2.123 -declare dvd_eq_mod_eq_0_number_of [simp]
   2.124 +lemmas dvd_eq_mod_eq_0_number_of [simp] =
   2.125 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y
   2.126  
   2.127  
   2.128  subsubsection {* Nitpick *}
     3.1 --- a/src/HOL/HOL.thy	Sun Nov 20 21:07:06 2011 +0100
     3.2 +++ b/src/HOL/HOL.thy	Sun Nov 20 21:07:10 2011 +0100
     3.3 @@ -494,7 +494,7 @@
     3.4  apply assumption
     3.5  done
     3.6  
     3.7 -lemmas ccontr = FalseE [THEN classical, standard]
     3.8 +lemmas ccontr = FalseE [THEN classical]
     3.9  
    3.10  (*notE with premises exchanged; it discharges ~R so that it can be used to
    3.11    make elimination rules*)
    3.12 @@ -1445,8 +1445,8 @@
    3.13  
    3.14  lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
    3.15  lemmas induct_atomize = induct_atomize' induct_equal_eq
    3.16 -lemmas induct_rulify' [symmetric, standard] = induct_atomize'
    3.17 -lemmas induct_rulify [symmetric, standard] = induct_atomize
    3.18 +lemmas induct_rulify' [symmetric] = induct_atomize'
    3.19 +lemmas induct_rulify [symmetric] = induct_atomize
    3.20  lemmas induct_rulify_fallback =
    3.21    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    3.22    induct_true_def induct_false_def
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Nov 20 21:07:06 2011 +0100
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Nov 20 21:07:10 2011 +0100
     4.3 @@ -554,7 +554,7 @@
     4.4    apply (erule ex_has_least_nat)
     4.5    done
     4.6  
     4.7 -lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
     4.8 +lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]
     4.9  
    4.10  lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
    4.11  by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
    4.12 @@ -620,7 +620,7 @@
    4.13    apply (erule ex_has_greatest_nat, assumption)
    4.14    done
    4.15  
    4.16 -lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
    4.17 +lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1]
    4.18  
    4.19  lemma GreatestM_nat_le:
    4.20    "P x ==> \<forall>y. P y --> m y < b
     5.1 --- a/src/HOL/Int.thy	Sun Nov 20 21:07:06 2011 +0100
     5.2 +++ b/src/HOL/Int.thy	Sun Nov 20 21:07:10 2011 +0100
     5.3 @@ -273,10 +273,11 @@
     5.4  done
     5.5  
     5.6  lemmas int_distrib =
     5.7 -  left_distrib [of "z1::int" "z2" "w", standard]
     5.8 -  right_distrib [of "w::int" "z1" "z2", standard]
     5.9 -  left_diff_distrib [of "z1::int" "z2" "w", standard]
    5.10 -  right_diff_distrib [of "w::int" "z1" "z2", standard]
    5.11 +  left_distrib [of z1 z2 w]
    5.12 +  right_distrib [of w z1 z2]
    5.13 +  left_diff_distrib [of z1 z2 w]
    5.14 +  right_diff_distrib [of w z1 z2]
    5.15 +  for z1 z2 w :: int
    5.16  
    5.17  
    5.18  subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
    5.19 @@ -637,12 +638,9 @@
    5.20  definition pred :: "int \<Rightarrow> int" where
    5.21    "pred k = k - 1"
    5.22  
    5.23 -lemmas
    5.24 -  max_number_of [simp] = max_def
    5.25 -    [of "number_of u" "number_of v", standard]
    5.26 -and
    5.27 -  min_number_of [simp] = min_def 
    5.28 -    [of "number_of u" "number_of v", standard]
    5.29 +lemmas max_number_of [simp] = max_def [of "number_of u" "number_of v"]
    5.30 +  and min_number_of [simp] = min_def [of "number_of u" "number_of v"]
    5.31 +  for u v
    5.32    -- {* unfolding @{text minx} and @{text max} on numerals *}
    5.33  
    5.34  lemmas numeral_simps = 
    5.35 @@ -1178,8 +1176,7 @@
    5.36  text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
    5.37  
    5.38  lemmas le_number_of_eq_not_less =
    5.39 -  linorder_not_less [of "number_of w" "number_of v", symmetric, 
    5.40 -  standard]
    5.41 +  linorder_not_less [of "number_of w" "number_of v", symmetric] for w v
    5.42  
    5.43  
    5.44  text {* Absolute value (@{term abs}) *}
    5.45 @@ -1199,12 +1196,12 @@
    5.46  
    5.47  subsubsection {* Simplification of arithmetic operations on integer constants. *}
    5.48  
    5.49 -lemmas arith_extra_simps [standard, simp] =
    5.50 +lemmas arith_extra_simps [simp] =
    5.51    number_of_add [symmetric]
    5.52    number_of_minus [symmetric]
    5.53    numeral_m1_eq_minus_1 [symmetric]
    5.54    number_of_mult [symmetric]
    5.55 -  diff_number_of_eq abs_number_of 
    5.56 +  diff_number_of_eq abs_number_of
    5.57  
    5.58  text {*
    5.59    For making a minimal simpset, one must include these default simprules.
    5.60 @@ -1465,34 +1462,34 @@
    5.61  
    5.62  lemmas add_special =
    5.63      one_add_one_is_two
    5.64 -    binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
    5.65 -    binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
    5.66 +    binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl]
    5.67 +    binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1]
    5.68  
    5.69  text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
    5.70  lemmas diff_special =
    5.71 -    binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
    5.72 -    binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
    5.73 +    binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl]
    5.74 +    binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1]
    5.75  
    5.76  text{*Allow 0 or 1 on either side with a binary numeral on the other*}
    5.77  lemmas eq_special =
    5.78 -    binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
    5.79 -    binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
    5.80 -    binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
    5.81 -    binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
    5.82 +    binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl]
    5.83 +    binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl]
    5.84 +    binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0]
    5.85 +    binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1]
    5.86  
    5.87  text{*Allow 0 or 1 on either side with a binary numeral on the other*}
    5.88  lemmas less_special =
    5.89 -  binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
    5.90 -  binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
    5.91 -  binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
    5.92 -  binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
    5.93 +  binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl]
    5.94 +  binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl]
    5.95 +  binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0]
    5.96 +  binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1]
    5.97  
    5.98  text{*Allow 0 or 1 on either side with a binary numeral on the other*}
    5.99  lemmas le_special =
   5.100 -    binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
   5.101 -    binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
   5.102 -    binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
   5.103 -    binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
   5.104 +    binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl]
   5.105 +    binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl]
   5.106 +    binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0]
   5.107 +    binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1]
   5.108  
   5.109  lemmas arith_special[simp] = 
   5.110         add_special diff_special eq_special less_special le_special
   5.111 @@ -1609,7 +1606,7 @@
   5.112  
   5.113  text{*This simplifies expressions of the form @{term "int n = z"} where
   5.114        z is an integer literal.*}
   5.115 -lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
   5.116 +lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v"] for v
   5.117  
   5.118  lemma split_nat [arith_split]:
   5.119    "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   5.120 @@ -1895,60 +1892,33 @@
   5.121  
   5.122  text{*These distributive laws move literals inside sums and differences.*}
   5.123  
   5.124 -lemmas left_distrib_number_of [simp] =
   5.125 -  left_distrib [of _ _ "number_of v", standard]
   5.126 -
   5.127 -lemmas right_distrib_number_of [simp] =
   5.128 -  right_distrib [of "number_of v", standard]
   5.129 -
   5.130 -lemmas left_diff_distrib_number_of [simp] =
   5.131 -  left_diff_distrib [of _ _ "number_of v", standard]
   5.132 -
   5.133 -lemmas right_diff_distrib_number_of [simp] =
   5.134 -  right_diff_distrib [of "number_of v", standard]
   5.135 +lemmas left_distrib_number_of [simp] = left_distrib [of _ _ "number_of v"] for v
   5.136 +lemmas right_distrib_number_of [simp] = right_distrib [of "number_of v"] for v
   5.137 +lemmas left_diff_distrib_number_of [simp] = left_diff_distrib [of _ _ "number_of v"] for v
   5.138 +lemmas right_diff_distrib_number_of [simp] = right_diff_distrib [of "number_of v"] for v
   5.139  
   5.140  text{*These are actually for fields, like real: but where else to put them?*}
   5.141  
   5.142 -lemmas zero_less_divide_iff_number_of [simp, no_atp] =
   5.143 -  zero_less_divide_iff [of "number_of w", standard]
   5.144 -
   5.145 -lemmas divide_less_0_iff_number_of [simp, no_atp] =
   5.146 -  divide_less_0_iff [of "number_of w", standard]
   5.147 -
   5.148 -lemmas zero_le_divide_iff_number_of [simp, no_atp] =
   5.149 -  zero_le_divide_iff [of "number_of w", standard]
   5.150 -
   5.151 -lemmas divide_le_0_iff_number_of [simp, no_atp] =
   5.152 -  divide_le_0_iff [of "number_of w", standard]
   5.153 +lemmas zero_less_divide_iff_number_of [simp, no_atp] = zero_less_divide_iff [of "number_of w"] for w
   5.154 +lemmas divide_less_0_iff_number_of [simp, no_atp] = divide_less_0_iff [of "number_of w"] for w
   5.155 +lemmas zero_le_divide_iff_number_of [simp, no_atp] = zero_le_divide_iff [of "number_of w"] for w
   5.156 +lemmas divide_le_0_iff_number_of [simp, no_atp] = divide_le_0_iff [of "number_of w"] for w
   5.157  
   5.158  
   5.159  text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
   5.160    strange, but then other simprocs simplify the quotient.*}
   5.161  
   5.162 -lemmas inverse_eq_divide_number_of [simp] =
   5.163 -  inverse_eq_divide [of "number_of w", standard]
   5.164 +lemmas inverse_eq_divide_number_of [simp] = inverse_eq_divide [of "number_of w"] for w
   5.165  
   5.166  text {*These laws simplify inequalities, moving unary minus from a term
   5.167  into the literal.*}
   5.168  
   5.169 -lemmas less_minus_iff_number_of [simp, no_atp] =
   5.170 -  less_minus_iff [of "number_of v", standard]
   5.171 -
   5.172 -lemmas le_minus_iff_number_of [simp, no_atp] =
   5.173 -  le_minus_iff [of "number_of v", standard]
   5.174 -
   5.175 -lemmas equation_minus_iff_number_of [simp, no_atp] =
   5.176 -  equation_minus_iff [of "number_of v", standard]
   5.177 -
   5.178 -lemmas minus_less_iff_number_of [simp, no_atp] =
   5.179 -  minus_less_iff [of _ "number_of v", standard]
   5.180 -
   5.181 -lemmas minus_le_iff_number_of [simp, no_atp] =
   5.182 -  minus_le_iff [of _ "number_of v", standard]
   5.183 -
   5.184 -lemmas minus_equation_iff_number_of [simp, no_atp] =
   5.185 -  minus_equation_iff [of _ "number_of v", standard]
   5.186 -
   5.187 +lemmas less_minus_iff_number_of [simp, no_atp] = less_minus_iff [of "number_of v"] for v
   5.188 +lemmas le_minus_iff_number_of [simp, no_atp] = le_minus_iff [of "number_of v"] for v
   5.189 +lemmas equation_minus_iff_number_of [simp, no_atp] = equation_minus_iff [of "number_of v"] for v
   5.190 +lemmas minus_less_iff_number_of [simp, no_atp] = minus_less_iff [of _ "number_of v"] for v
   5.191 +lemmas minus_le_iff_number_of [simp, no_atp] = minus_le_iff [of _ "number_of v"] for v
   5.192 +lemmas minus_equation_iff_number_of [simp, no_atp] = minus_equation_iff [of _ "number_of v"] for v
   5.193  
   5.194  text{*To Simplify Inequalities Where One Side is the Constant 1*}
   5.195  
   5.196 @@ -1985,39 +1955,32 @@
   5.197  
   5.198  text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
   5.199  
   5.200 -lemmas mult_less_cancel_left_number_of [simp, no_atp] =
   5.201 -  mult_less_cancel_left [of "number_of v", standard]
   5.202 -
   5.203 -lemmas mult_less_cancel_right_number_of [simp, no_atp] =
   5.204 -  mult_less_cancel_right [of _ "number_of v", standard]
   5.205 -
   5.206 -lemmas mult_le_cancel_left_number_of [simp, no_atp] =
   5.207 -  mult_le_cancel_left [of "number_of v", standard]
   5.208 -
   5.209 -lemmas mult_le_cancel_right_number_of [simp, no_atp] =
   5.210 -  mult_le_cancel_right [of _ "number_of v", standard]
   5.211 +lemmas mult_less_cancel_left_number_of [simp, no_atp] = mult_less_cancel_left [of "number_of v"] for v
   5.212 +lemmas mult_less_cancel_right_number_of [simp, no_atp] = mult_less_cancel_right [of _ "number_of v"] for v
   5.213 +lemmas mult_le_cancel_left_number_of [simp, no_atp] = mult_le_cancel_left [of "number_of v"] for v
   5.214 +lemmas mult_le_cancel_right_number_of [simp, no_atp] = mult_le_cancel_right [of _ "number_of v"] for v
   5.215  
   5.216  
   5.217  text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
   5.218  
   5.219 -lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
   5.220 -lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
   5.221 -lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
   5.222 -lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
   5.223 -lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
   5.224 -lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
   5.225 +lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w"] for w
   5.226 +lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w"] for w
   5.227 +lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w"] for w
   5.228 +lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w"] for w
   5.229 +lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w"] for w
   5.230 +lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w"] for w
   5.231  
   5.232  
   5.233  subsubsection{*Optional Simplification Rules Involving Constants*}
   5.234  
   5.235  text{*Simplify quotients that are compared with a literal constant.*}
   5.236  
   5.237 -lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
   5.238 -lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
   5.239 -lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
   5.240 -lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
   5.241 -lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
   5.242 -lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
   5.243 +lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w"] for w
   5.244 +lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w"] for w
   5.245 +lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w"] for w
   5.246 +lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w"] for w
   5.247 +lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w"] for w
   5.248 +lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w"] for w
   5.249  
   5.250  
   5.251  text{*Not good as automatic simprules because they cause case splits.*}
   5.252 @@ -2040,7 +2003,7 @@
   5.253       "(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
   5.254  by auto
   5.255  
   5.256 -lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
   5.257 +lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
   5.258  
   5.259  lemma divide_Numeral1:
   5.260    "(x::'a::{field, number_ring}) / Numeral1 = x"
   5.261 @@ -2359,16 +2322,16 @@
   5.262  lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
   5.263  lemmas int_mult = of_nat_mult [where 'a=int]
   5.264  lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
   5.265 -lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
   5.266 +lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
   5.267  lemmas zless_int = of_nat_less_iff [where 'a=int]
   5.268 -lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
   5.269 +lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
   5.270  lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
   5.271  lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   5.272 -lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
   5.273 +lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
   5.274  lemmas int_0 = of_nat_0 [where 'a=int]
   5.275  lemmas int_1 = of_nat_1 [where 'a=int]
   5.276  lemmas int_Suc = of_nat_Suc [where 'a=int]
   5.277 -lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
   5.278 +lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
   5.279  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   5.280  lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
   5.281  
     6.1 --- a/src/HOL/List.thy	Sun Nov 20 21:07:06 2011 +0100
     6.2 +++ b/src/HOL/List.thy	Sun Nov 20 21:07:10 2011 +0100
     6.3 @@ -2564,7 +2564,7 @@
     6.4  -- {* simp does not terminate! *}
     6.5  by (induct j) auto
     6.6  
     6.7 -lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
     6.8 +lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n"] for m n
     6.9  
    6.10  lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
    6.11  by (subst upt_rec) simp
    6.12 @@ -2679,9 +2679,9 @@
    6.13  lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
    6.14  by (cases n) simp_all
    6.15  
    6.16 -lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
    6.17 -lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
    6.18 -lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
    6.19 +lemmas take_Cons_number_of = take_Cons'[of "number_of v"] for v
    6.20 +lemmas drop_Cons_number_of = drop_Cons'[of "number_of v"] for v
    6.21 +lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v"] for v
    6.22  
    6.23  declare take_Cons_number_of [simp] 
    6.24          drop_Cons_number_of [simp] 
    6.25 @@ -2700,8 +2700,7 @@
    6.26  
    6.27  declare upto.simps[code, simp del]
    6.28  
    6.29 -lemmas upto_rec_number_of[simp] =
    6.30 -  upto.simps[of "number_of m" "number_of n", standard]
    6.31 +lemmas upto_rec_number_of[simp] = upto.simps[of "number_of m" "number_of n"] for m n
    6.32  
    6.33  lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
    6.34  by(simp add: upto.simps)
     7.1 --- a/src/HOL/Nat_Numeral.thy	Sun Nov 20 21:07:06 2011 +0100
     7.2 +++ b/src/HOL/Nat_Numeral.thy	Sun Nov 20 21:07:10 2011 +0100
     7.3 @@ -510,7 +510,7 @@
     7.4  
     7.5  text{*Squares of literal numerals will be evaluated.*}
     7.6  lemmas power2_eq_square_number_of [simp] =
     7.7 -    power2_eq_square [of "number_of w", standard]
     7.8 +  power2_eq_square [of "number_of w"] for w
     7.9  
    7.10  
    7.11  text{*Simprules for comparisons where common factors can be cancelled.*}
    7.12 @@ -529,7 +529,7 @@
    7.13  
    7.14  (*Expresses a natural number constant as the Suc of another one.
    7.15    NOT suitable for rewriting because n recurs in the condition.*)
    7.16 -lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
    7.17 +lemmas expand_Suc = Suc_pred' [of "number_of v"] for v
    7.18  
    7.19  subsubsection{*Arith *}
    7.20  
    7.21 @@ -684,7 +684,7 @@
    7.22           split add: split_if cong: imp_cong)
    7.23  
    7.24  
    7.25 -lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
    7.26 +lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w"] for w
    7.27  declare power_nat_number_of_number_of [simp]
    7.28  
    7.29  
    7.30 @@ -711,10 +711,10 @@
    7.31  lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
    7.32  
    7.33  lemmas power_number_of_even_number_of [simp] =
    7.34 -    power_number_of_even [of "number_of v", standard]
    7.35 +    power_number_of_even [of "number_of v"] for v
    7.36  
    7.37  lemmas power_number_of_odd_number_of [simp] =
    7.38 -    power_number_of_odd [of "number_of v", standard]
    7.39 +    power_number_of_odd [of "number_of v"] for v
    7.40  
    7.41  lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
    7.42    by (simp add: nat_number_of_def)
     8.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Nov 20 21:07:06 2011 +0100
     8.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Nov 20 21:07:10 2011 +0100
     8.3 @@ -14,8 +14,8 @@
     8.4    ("Tools/nat_numeral_simprocs.ML")
     8.5  begin
     8.6  
     8.7 -declare split_div [of _ _ "number_of k", standard, arith_split]
     8.8 -declare split_mod [of _ _ "number_of k", standard, arith_split]
     8.9 +declare split_div [of _ _ "number_of k", arith_split] for k
    8.10 +declare split_mod [of _ _ "number_of k", arith_split] for k
    8.11  
    8.12  text {* For @{text combine_numerals} *}
    8.13  
     9.1 --- a/src/HOL/Parity.thy	Sun Nov 20 21:07:06 2011 +0100
     9.2 +++ b/src/HOL/Parity.thy	Sun Nov 20 21:07:10 2011 +0100
     9.3 @@ -45,9 +45,9 @@
     9.4  
     9.5  lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
     9.6  
     9.7 -declare even_def[of "number_of v", standard, simp]
     9.8 +declare even_def[of "number_of v", simp] for v
     9.9  
    9.10 -declare even_nat_def[of "number_of v", standard, simp]
    9.11 +declare even_nat_def[of "number_of v", simp] for v
    9.12  
    9.13  subsection {* Even and odd are mutually exclusive *}
    9.14  
    9.15 @@ -347,27 +347,27 @@
    9.16  
    9.17  text {* Simplify, when the exponent is a numeral *}
    9.18  
    9.19 -lemmas power_0_left_number_of = power_0_left [of "number_of w", standard]
    9.20 +lemmas power_0_left_number_of = power_0_left [of "number_of w"] for w
    9.21  declare power_0_left_number_of [simp]
    9.22  
    9.23  lemmas zero_le_power_eq_number_of [simp] =
    9.24 -    zero_le_power_eq [of _ "number_of w", standard]
    9.25 +    zero_le_power_eq [of _ "number_of w"] for w
    9.26  
    9.27  lemmas zero_less_power_eq_number_of [simp] =
    9.28 -    zero_less_power_eq [of _ "number_of w", standard]
    9.29 +    zero_less_power_eq [of _ "number_of w"] for w
    9.30  
    9.31  lemmas power_le_zero_eq_number_of [simp] =
    9.32 -    power_le_zero_eq [of _ "number_of w", standard]
    9.33 +    power_le_zero_eq [of _ "number_of w"] for w
    9.34  
    9.35  lemmas power_less_zero_eq_number_of [simp] =
    9.36 -    power_less_zero_eq [of _ "number_of w", standard]
    9.37 +    power_less_zero_eq [of _ "number_of w"] for w
    9.38  
    9.39  lemmas zero_less_power_nat_eq_number_of [simp] =
    9.40 -    zero_less_power_nat_eq [of _ "number_of w", standard]
    9.41 +    zero_less_power_nat_eq [of _ "number_of w"] for w
    9.42  
    9.43 -lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard]
    9.44 +lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w"] for w
    9.45  
    9.46 -lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard]
    9.47 +lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _] for w
    9.48  
    9.49  
    9.50  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
    10.1 --- a/src/HOL/Product_Type.thy	Sun Nov 20 21:07:06 2011 +0100
    10.2 +++ b/src/HOL/Product_Type.thy	Sun Nov 20 21:07:10 2011 +0100
    10.3 @@ -625,7 +625,7 @@
    10.4    Setup of internal @{text split_rule}.
    10.5  *}
    10.6  
    10.7 -lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    10.8 +lemmas prod_caseI = prod.cases [THEN iffD2]
    10.9  
   10.10  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
   10.11    by (fact splitI2)
    11.1 --- a/src/HOL/Set.thy	Sun Nov 20 21:07:06 2011 +0100
    11.2 +++ b/src/HOL/Set.thy	Sun Nov 20 21:07:10 2011 +0100
    11.3 @@ -1107,7 +1107,7 @@
    11.4  lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
    11.5    by blast
    11.6  
    11.7 -lemmas empty_not_insert = insert_not_empty [symmetric, standard]
    11.8 +lemmas empty_not_insert = insert_not_empty [symmetric]
    11.9  declare empty_not_insert [simp]
   11.10  
   11.11  lemma insert_absorb: "a \<in> A ==> insert a A = A"
    12.1 --- a/src/HOL/Transitive_Closure.thy	Sun Nov 20 21:07:06 2011 +0100
    12.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Nov 20 21:07:10 2011 +0100
    12.3 @@ -139,7 +139,7 @@
    12.4    qed
    12.5  qed
    12.6  
    12.7 -lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
    12.8 +lemmas rtrancl_trans = trans_rtrancl [THEN transD]
    12.9  
   12.10  lemma rtranclp_trans:
   12.11    assumes xy: "r^** x y"
   12.12 @@ -429,7 +429,7 @@
   12.13    qed
   12.14  qed
   12.15  
   12.16 -lemmas trancl_trans = trans_trancl [THEN transD, standard]
   12.17 +lemmas trancl_trans = trans_trancl [THEN transD]
   12.18  
   12.19  lemma tranclp_trans:
   12.20    assumes xy: "r^++ x y"