changeset 40690 | 3f472e57446a |
parent 40077 | c8a9eaaa2f59 |
child 43526 | 2b92a6943915 |
--- a/src/HOL/Nat_Numeral.thy Wed Nov 24 23:17:24 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Thu Nov 25 00:17:16 2010 +0100 @@ -674,7 +674,7 @@ lemma nat_number_of_Pls: "Numeral0 = (0::nat)" by (simp add: nat_number_of_def) -lemma nat_number_of_Min: "number_of Int.Min = (0::nat)" +lemma nat_number_of_Min [no_atp]: "number_of Int.Min = (0::nat)" apply (simp only: number_of_Min nat_number_of_def nat_zminus_int) done