src/HOL/Tools/SMT/z3_replay_methods.ML
18 months ago wenzelm 2017-11-26 more symbols;
20 months ago blanchet 2017-09-26 strengthened reconstruction tactic
2017-05-10 blanchet 2017-05-10 made SMT reconstruction more complete (bug report by Lukas Bulwahn)
2016-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-10-17 wenzelm 2015-10-17 tuned signature;
2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
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);
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06 wenzelm 2015-03-06 tuned -- more explicit use of context;
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
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-09-02 boehmes 2014-09-02 replay Z3 rewrite steps that lift if-then-else expressions
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'