src/HOL/Tools/ATP/atp_proof_reconstruct.ML
2012-08-14 blanchet 2012-08-14 warn users about unused "using" facts
2012-07-27 blanchet 2012-07-27 extract Z3 unsat cores (for "z3_tptp")
2012-07-23 blanchet 2012-07-23 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-06-26 blanchet 2012-06-26 added sorts to datastructure
2012-06-26 blanchet 2012-06-26 added type arguments to "ATerm" constructor -- but don't use them yet
2012-06-06 blanchet 2012-06-06 avoid dumping definitions several times in LEO-II proofs
2012-05-23 blanchet 2012-05-23 improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
2012-05-23 blanchet 2012-05-23 augment Satallax unsat cores with all definitions
2012-05-21 blanchet 2012-05-21 include "ext" in all Satallax proofs
2012-05-15 blanchet 2012-05-15 repair the Waldmeister endgame only for Waldmeister proofs
2012-05-14 blanchet 2012-05-14 ensure the "show" equation is not reoriented by Waldmeister
2012-05-14 blanchet 2012-05-14 ensure consistent naming of Waldmeister proof steps, so that they are not cleaned away by "clean_up_atp_proof_dependencies"
2012-05-14 blanchet 2012-05-14 graceful handling of Waldmeister endgame
2012-04-26 blanchet 2012-04-26 tuning
2012-03-27 blanchet 2012-03-27 print a hint
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-02-27 wenzelm 2012-02-27 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-02-06 blanchet 2012-02-06 renamed type encoding
2012-02-05 blanchet 2012-02-05 cleaned up new SPASS parsing
2012-01-30 blanchet 2012-01-30 avoid unsupported case in Metis
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-27 blanchet 2012-01-27 made SML/NJ happy
2012-01-26 blanchet 2012-01-26 separate orthogonal components
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file