src/HOL/Tools/SMT/z3_replay_util.ML
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'