src/HOL/Tools/SMT/z3_proof_tools.ML
changeset 47108 2a1953f0d20d
parent 46497 89ccf66aa73d
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -334,14 +334,12 @@
     1.4  
     1.5    val basic_simpset = HOL_ss addsimps @{thms field_simps}
     1.6      addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
     1.7 -    addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
     1.8 -    addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
     1.9 -    addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
    1.10 -    addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
    1.11 -    addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
    1.12 +    addsimps @{thms arith_special} addsimps @{thms arith_simps}
    1.13 +    addsimps @{thms rel_simps}
    1.14      addsimps @{thms array_rules}
    1.15      addsimps @{thms term_true_def} addsimps @{thms term_false_def}
    1.16      addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
    1.17 +    addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod}]
    1.18      addsimprocs [
    1.19        Simplifier.simproc_global @{theory} "fast_int_arith" [
    1.20          "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),