src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
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;