src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-01-24 wenzelm 2016-01-24 clarified exception handling;
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-05-30 wenzelm 2015-05-30 standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
2015-05-30 wenzelm 2015-05-30 tuned spelling;
2015-03-31 wenzelm 2015-03-31 tuned -- avoid exotic Name_Space.defined_entry;
2015-03-30 wenzelm 2015-03-30 support for strictly private name space entries; tuned signature;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-20 wenzelm 2015-03-20 tuned;
2015-03-19 wenzelm 2015-03-19 more position information;
2015-03-06 wenzelm 2015-03-06 clarified context;
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-02-11 wenzelm 2015-02-11 proper context; tuned;
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-08 wenzelm 2014-11-08 more direct type equality;
2014-09-21 wenzelm 2014-09-21 more standard Isabelle/ML operations;
2014-09-21 wenzelm 2014-09-21 tuned;
2014-06-22 sultana 2014-06-22 Metis is being used to emulate E steps;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-19 wenzelm 2014-03-19 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2014-02-19 sultana 2014-02-19 added a function that carries out all the reconstruction steps, for improved usability; added documentation;
2014-02-19 sultana 2014-02-19 reconstruction framework for LEO-II's TPTP proofs;