src/HOL/Num.thy
changeset 63913 6b886cadba7c
parent 63654 f90e3926e627
child 64178 12e6c3bbb488
     1.1 --- a/src/HOL/Num.thy	Sun Sep 18 11:31:19 2016 +0200
     1.2 +++ b/src/HOL/Num.thy	Sun Sep 18 18:23:59 2016 +0200
     1.3 @@ -994,6 +994,8 @@
     1.4  lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"
     1.5    by (rule numeral_One) (rule numeral_2_eq_2)
     1.6  
     1.7 +lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def
     1.8 +
     1.9  text \<open>Comparisons involving @{term Suc}.\<close>
    1.10  
    1.11  lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"