src/HOL/Tools/SMT/z3_replay.ML
18 months ago wenzelm 2017-11-26 more symbols;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-04-25 blanchet 2015-04-25 made CVC4 support work also without unsat cores
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-16 boehmes 2015-01-16 more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
2015-01-15 boehmes 2015-01-15 more detailed runtime statistics for Z3 proof reconstruction
2014-12-29 boehmes 2014-12-29 optionally display statistics for Z3 proof reconstruction
2014-12-29 boehmes 2014-12-29 limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
2014-09-29 blanchet 2014-09-29 simplified and repaired veriT index handling code
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'