src/HOL/Int.thy
changeset 30802 f9e9e800d27e
parent 30796 126701134811
child 30839 bf99ceb7d015
     1.1 --- a/src/HOL/Int.thy	Mon Mar 30 10:47:41 2009 -0700
     1.2 +++ b/src/HOL/Int.thy	Mon Mar 30 12:07:59 2009 -0700
     1.3 @@ -1525,6 +1525,17 @@
     1.4  lemmas zle_int = of_nat_le_iff [where 'a=int]
     1.5  lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
     1.6  
     1.7 +subsection {* Setting up simplification procedures *}
     1.8 +
     1.9 +lemmas int_arith_rules =
    1.10 +  neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
    1.11 +  minus_zero diff_minus left_minus right_minus
    1.12 +  mult_zero_left mult_zero_right mult_Bit1 mult_1_right
    1.13 +  mult_minus_left mult_minus_right
    1.14 +  minus_add_distrib minus_minus mult_assoc
    1.15 +  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.16 +  of_int_0 of_int_1 of_int_add of_int_mult
    1.17 +
    1.18  use "Tools/int_arith.ML"
    1.19  declaration {* K Int_Arith.setup *}
    1.20