src/HOL/Tools/SMT/z3_replay_methods.ML
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'