changeset 36841 | 02df88789641 |
parent 36823 | 001d1aad99de |
child 36964 | a354605f03dc |
--- a/src/HOL/Nat_Numeral.thy Tue May 11 19:00:32 2010 -0700 +++ b/src/HOL/Nat_Numeral.thy Tue May 11 19:01:35 2010 -0700 @@ -712,7 +712,7 @@ if_True add_0 add_Suc add_number_of_left mult_number_of_left numeral_1_eq_1 [symmetric] Suc_eq_plus1 numeral_0_eq_0 [symmetric] numerals [symmetric] - iszero_simps not_iszero_Numeral1 + not_iszero_Numeral1 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" by (fact Let_def)