src/HOL/Nat_Numeral.thy
changeset 45607 16b4f5774621
parent 44884 02efd5a6b6e5
child 46026 83caa4f4bd56
     1.1 --- a/src/HOL/Nat_Numeral.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -510,7 +510,7 @@
     1.4  
     1.5  text{*Squares of literal numerals will be evaluated.*}
     1.6  lemmas power2_eq_square_number_of [simp] =
     1.7 -    power2_eq_square [of "number_of w", standard]
     1.8 +  power2_eq_square [of "number_of w"] for w
     1.9  
    1.10  
    1.11  text{*Simprules for comparisons where common factors can be cancelled.*}
    1.12 @@ -529,7 +529,7 @@
    1.13  
    1.14  (*Expresses a natural number constant as the Suc of another one.
    1.15    NOT suitable for rewriting because n recurs in the condition.*)
    1.16 -lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
    1.17 +lemmas expand_Suc = Suc_pred' [of "number_of v"] for v
    1.18  
    1.19  subsubsection{*Arith *}
    1.20  
    1.21 @@ -684,7 +684,7 @@
    1.22           split add: split_if cong: imp_cong)
    1.23  
    1.24  
    1.25 -lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
    1.26 +lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w"] for w
    1.27  declare power_nat_number_of_number_of [simp]
    1.28  
    1.29  
    1.30 @@ -711,10 +711,10 @@
    1.31  lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
    1.32  
    1.33  lemmas power_number_of_even_number_of [simp] =
    1.34 -    power_number_of_even [of "number_of v", standard]
    1.35 +    power_number_of_even [of "number_of v"] for v
    1.36  
    1.37  lemmas power_number_of_odd_number_of [simp] =
    1.38 -    power_number_of_odd [of "number_of v", standard]
    1.39 +    power_number_of_odd [of "number_of v"] for v
    1.40  
    1.41  lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
    1.42    by (simp add: nat_number_of_def)