diff -r 73e738371c90 -r 3e9e8dfb3c98 src/HOL/Tools/SMT/z3_proof_tools.ML
--- 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),