src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
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;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-08-28 blanchet 2014-08-28 prefixed all old SMT commands, attributes, etc., with 'old_'
2014-08-28 blanchet 2014-08-28 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;