src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
2010-09-17 blanchet 2010-09-17 move functions around
2010-09-16 blanchet 2010-09-16 added new "Metis_Reconstruct" module, temporarily empty
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-16 blanchet 2010-09-16 move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
2010-09-16 blanchet 2010-09-16 merge constructors
2010-09-16 blanchet 2010-09-16 factor out the inverse of "nice_atp_problem"
2010-09-16 blanchet 2010-09-16 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
2010-09-16 blanchet 2010-09-16 factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
2010-09-15 blanchet 2010-09-15 fix parsing of higher-order formulas; this code was never exercised before because the current ATPs perform clausification, but someday ATPs might support FOF natively
2010-09-14 blanchet 2010-09-14 fix splitting of proof lines for one-line metis calls; needed for newly supported ATPs (Vampire 0.6 local and remote, SNARK)
2010-09-14 blanchet 2010-09-14 finish support for E 1.2 proof reconstruction; this involves picking up the axiom and conjecture names specified using a "file" annotation in the TSTP file, since we cannot rely anymore on formula numbers (E 1.2 adds a strange offset)
2010-09-14 blanchet 2010-09-14 first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
2010-09-14 blanchet 2010-09-14 use same hack as in "Async_Manager" to work around Proof General bug
2010-09-14 blanchet 2010-09-14 generalize proof reconstruction code; first step towards support for nonnumeric formula names, needed for E 1.2
2010-09-13 blanchet 2010-09-13 merged
2010-09-11 blanchet 2010-09-11 tuning
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-03 wenzelm 2010-09-03 turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
2010-09-02 blanchet 2010-09-02 fix trivial "x = x" fact detection
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-31 blanchet 2010-08-31 shorten a few file names