src/HOL/Tools/res_atp.ML
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-10 paulson 2007-08-10 removal of some refs
2007-06-14 paulson 2007-06-14 Now ResHolClause also does first-order problems!
2007-05-17 paulson 2007-05-17 Added three items to the signature
2007-05-08 wenzelm 2007-05-08 renamed call_atp to sledgehammer;
2007-04-30 paulson 2007-04-30 Removal of dead code
2007-04-19 paulson 2007-04-19 trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions
2007-04-18 paulson 2007-04-18 Fixes for proof reconstruction, especially involving abstractions and definitions
2007-04-12 paulson 2007-04-12 Improved treatment of classrel/arity clauses
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-02 paulson 2007-03-02 New code to store theorem names in a concise form rather than as fully-qualified. Meson.is_fol_term now takes a theory as argument.
2007-01-31 paulson 2007-01-31 Tidying; more debugging information. New reference unwanted_types.
2007-01-26 paulson 2007-01-26 Streamlined and improved debugging messages
2007-01-20 wenzelm 2007-01-20 Output.debug: non-strict; renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
2007-01-05 paulson 2007-01-05 Proof.context now sent to watcher and used in type inference step of proof reconstruction
2007-01-04 paulson 2007-01-04 improvements to proof reconstruction. Some files loaded in a different order
2007-01-03 paulson 2007-01-03 x-symbol is no longer switched off in the ATP linkup
2006-12-22 paulson 2006-12-22 tidying the ATP communications
2006-12-20 paulson 2006-12-20 change from "Array" to "Vector"
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-12 paulson 2006-12-12 Removal of the "keep_types" flag: we always keep types!
2006-12-07 paulson 2006-12-07 Removal of theorem tagging, which the ATP linkup no longer requires. Suffixes no longer blacklisted.
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-27 mengj 2006-11-27 Goals in clause form are sent to the relevance filter.
2006-11-24 paulson 2006-11-24 ATP linkup now generates "new TPTP" rather than "old TPTP"
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-11-22 paulson 2006-11-22 Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties
2006-11-21 paulson 2006-11-21 Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
2006-11-16 paulson 2006-11-16 Now includes only types used to instantiate overloaded constants in arity clauses
2006-11-15 paulson 2006-11-15 Arity clauses are now produced only for types and type classes actually used.
2006-11-11 mengj 2006-11-11 Added in is_fol_thms.
2006-11-10 paulson 2006-11-10 Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-11-07 paulson 2006-11-07 Proper theorem names at last, no fakes!! Added set_prover function to set various parameters to improve success rate. Fixed the auto settings for E.
2006-11-01 paulson 2006-11-01 More blacklisting CASC mode now always on, due to switch to Vampire 8.1 (i.e. the 2006 version) Now runs ATPs unless time_limit = 0.
2006-10-20 paulson 2006-10-20 Added more debugging info
2006-10-12 paulson 2006-10-12 Logging of theorem names to the /tmp directory now works
2006-10-10 paulson 2006-10-10 A way to call the ATP linkup from ML scripts
2006-10-06 paulson 2006-10-06 Tidied code to delete tmp files. Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
2006-10-06 paulson 2006-10-06 Improved detection of identical clauses, also in the conjecture
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-10-02 paulson 2006-10-02 restored the "length of name > 2" check for package definitions
2006-09-29 wenzelm 2006-09-29 simplified is_package_def -- be less ambitious about B library operations;
2006-09-28 paulson 2006-09-28 Definitions produced by packages are now blacklisted.
2006-09-21 paulson 2006-09-21 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.
2006-09-20 mengj 2006-09-20 Removed include_min_comb and include_combS.
2006-09-14 wenzelm 2006-09-14 made SML/NJ happy;
2006-09-13 paulson 2006-09-13 Extended the blacklist with higher-order theorems. Restructured. Added checks to ensure that no higher-order clauses are output in first-order mode.
2006-09-01 paulson 2006-09-01 refinements to conversion into clause form, esp for the HO case
2006-08-31 webertj 2006-08-31 String.concatWith (not available in PolyML) replaced by space_implode
2006-08-31 paulson 2006-08-31 blacklist now handles thm lists
2006-08-28 paulson 2006-08-28 minor bug fixes
2006-08-25 paulson 2006-08-25 abstraction of lambda-expressions
2006-08-09 paulson 2006-08-09 blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-28 paulson 2006-07-28 "all theorems" mode forces definition-expansion off. signature tidying
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-15 mengj 2006-07-15 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
2006-07-06 paulson 2006-07-06 some tidying; fixed the output of theorem names