# HG changeset patch # User boehmes # Date 1269652200 -3600 # Node ID 27e2fa7d4ce7fa3366a58f2cacb8516631782f79 # Parent c7d01a43e41b55bc03670a1342639e1296c32975 slightly more general simproc (avoids errors of linarith) diff -r c7d01a43e41b -r 27e2fa7d4ce7 src/HOL/SMT/Tools/z3_proof_rules.ML --- a/src/HOL/SMT/Tools/z3_proof_rules.ML Sat Mar 27 00:08:39 2010 +0100 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Sat Mar 27 02:10:00 2010 +0100 @@ -1143,6 +1143,7 @@ addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps} addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps} addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps} + addsimps [@{thm mult_1_left}] addsimprocs [ Simplifier.simproc @{theory} "fast_int_arith" [ "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc), diff -r c7d01a43e41b -r 27e2fa7d4ce7 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Sat Mar 27 00:08:39 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat Mar 27 02:10:00 2010 +0100 @@ -344,8 +344,7 @@ struct val assoc_ss = HOL_ss addsimps @{thms mult_ac} val eq_reflection = eq_reflection - fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true - | is_numeral _ = false; + val is_numeral = can HOLogic.dest_number end; structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);