src/HOL/Parity.thy
changeset 45607 16b4f5774621
parent 41959 b460124855b8
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Parity.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/Parity.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -45,9 +45,9 @@
     1.4  
     1.5  lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
     1.6  
     1.7 -declare even_def[of "number_of v", standard, simp]
     1.8 +declare even_def[of "number_of v", simp] for v
     1.9  
    1.10 -declare even_nat_def[of "number_of v", standard, simp]
    1.11 +declare even_nat_def[of "number_of v", simp] for v
    1.12  
    1.13  subsection {* Even and odd are mutually exclusive *}
    1.14  
    1.15 @@ -347,27 +347,27 @@
    1.16  
    1.17  text {* Simplify, when the exponent is a numeral *}
    1.18  
    1.19 -lemmas power_0_left_number_of = power_0_left [of "number_of w", standard]
    1.20 +lemmas power_0_left_number_of = power_0_left [of "number_of w"] for w
    1.21  declare power_0_left_number_of [simp]
    1.22  
    1.23  lemmas zero_le_power_eq_number_of [simp] =
    1.24 -    zero_le_power_eq [of _ "number_of w", standard]
    1.25 +    zero_le_power_eq [of _ "number_of w"] for w
    1.26  
    1.27  lemmas zero_less_power_eq_number_of [simp] =
    1.28 -    zero_less_power_eq [of _ "number_of w", standard]
    1.29 +    zero_less_power_eq [of _ "number_of w"] for w
    1.30  
    1.31  lemmas power_le_zero_eq_number_of [simp] =
    1.32 -    power_le_zero_eq [of _ "number_of w", standard]
    1.33 +    power_le_zero_eq [of _ "number_of w"] for w
    1.34  
    1.35  lemmas power_less_zero_eq_number_of [simp] =
    1.36 -    power_less_zero_eq [of _ "number_of w", standard]
    1.37 +    power_less_zero_eq [of _ "number_of w"] for w
    1.38  
    1.39  lemmas zero_less_power_nat_eq_number_of [simp] =
    1.40 -    zero_less_power_nat_eq [of _ "number_of w", standard]
    1.41 +    zero_less_power_nat_eq [of _ "number_of w"] for w
    1.42  
    1.43 -lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard]
    1.44 +lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w"] for w
    1.45  
    1.46 -lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard]
    1.47 +lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _] for w
    1.48  
    1.49  
    1.50  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}