src/HOL/Nat.thy
changeset 31024 0fdf666e08bf
parent 30975 b2fa60d56735
child 31100 6a2e67fe4488
     1.1 --- a/src/HOL/Nat.thy	Wed Apr 29 13:36:29 2009 -0700
     1.2 +++ b/src/HOL/Nat.thy	Wed Apr 29 17:15:01 2009 -0700
     1.3 @@ -1274,10 +1274,10 @@
     1.4  text{*Special cases where either operand is zero*}
     1.5  
     1.6  lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
     1.7 -  by (rule of_nat_eq_iff [of 0, simplified])
     1.8 +  by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
     1.9  
    1.10  lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    1.11 -  by (rule of_nat_eq_iff [of _ 0, simplified])
    1.12 +  by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
    1.13  
    1.14  lemma inj_of_nat: "inj of_nat"
    1.15    by (simp add: inj_on_def)