src/HOL/Numeral_Simprocs.thy
changeset 47255 30a1692557b0
parent 47159 978c00c20a59
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Apr 01 09:12:03 2012 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Apr 01 16:09:58 2012 +0200
     1.3 @@ -14,6 +14,14 @@
     1.4    ("Tools/nat_numeral_simprocs.ML")
     1.5  begin
     1.6  
     1.7 +lemmas semiring_norm =
     1.8 +  Let_def arith_simps nat_arith rel_simps
     1.9 +  if_False if_True
    1.10 +  add_0 add_Suc add_numeral_left
    1.11 +  add_neg_numeral_left mult_numeral_left
    1.12 +  numeral_1_eq_1 [symmetric] Suc_eq_plus1
    1.13 +  eq_numeral_iff_iszero not_iszero_Numeral1
    1.14 +
    1.15  declare split_div [of _ _ "numeral k", arith_split] for k
    1.16  declare split_mod [of _ _ "numeral k", arith_split] for k
    1.17