summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Nat.thy

changeset 31024 | 0fdf666e08bf |

parent 30975 | b2fa60d56735 |

child 31100 | 6a2e67fe4488 |

--- a/src/HOL/Nat.thy Wed Apr 29 13:36:29 2009 -0700 +++ b/src/HOL/Nat.thy Wed Apr 29 17:15:01 2009 -0700 @@ -1274,10 +1274,10 @@ text{*Special cases where either operand is zero*} lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n" - by (rule of_nat_eq_iff [of 0, simplified]) + by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0]) lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0" - by (rule of_nat_eq_iff [of _ 0, simplified]) + by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0]) lemma inj_of_nat: "inj of_nat" by (simp add: inj_on_def)