src/HOL/Tools/SMT/z3_replay_util.ML
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
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'