src/HOL/Tools/SMT/z3_replay_util.ML
changeset 58776 95e58e04e534
parent 58061 3d060f43accb
child 60642 48dd1cefb4ae
     1.1 --- a/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4    val basic_simpset =
     1.5      simpset_of (put_simpset HOL_ss @{context}
     1.6        addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
     1.7 -        arith_simps rel_simps array_rules z3div_def z3mod_def}
     1.8 +        arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
     1.9        addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
    1.10          Simplifier.simproc_global @{theory} "fast_int_arith" [
    1.11            "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,