summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)