--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Thu May 27 14:54:13 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Thu May 27 14:55:53 2010 +0200
@@ -321,6 +321,7 @@
addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
addsimps @{thms array_rules}
+ addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
addsimprocs [
Simplifier.simproc @{theory} "fast_int_arith" [
"(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),