src/HOL/Tools/res_atp.ML
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
2006-06-15 paulson 2006-06-15 the "all_theorems" option and some fixes
2006-06-04 mengj 2006-06-04 ATP/res_clasimpset.ML has been merged into res_atp.ML.
2006-05-29 paulson 2006-05-29 warnings to debug outputs
2006-05-29 paulson 2006-05-29 Giving the "--silent" switch to E, to produce less output
2006-05-25 mengj 2006-05-25 Added in settings used by "spass" method.
2006-05-25 mengj 2006-05-25 Added support for DFG format, used by SPASS.
2006-05-17 paulson 2006-05-17 removing the string array from the result of get_clasimp_atp_lemmas
2006-05-16 wenzelm 2006-05-16 replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-04-28 mengj 2006-04-28 removed the functions for getting HOL helper paths.
2006-04-20 mengj 2006-04-20 Changed the logic detection method.
2006-04-19 paulson 2006-04-19 exported linkup_logic_mode and changed the default setting
2006-04-19 paulson 2006-04-19 tidying; ATP options including CASC mode for Vampire
2006-04-18 mengj 2006-04-18 Tidied up some programs.
2006-04-07 mengj 2006-04-07 lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
2006-03-09 mengj 2006-03-09 Added more functions to the signature and tidied up some functions.
2006-03-07 paulson 2006-03-07 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
2006-03-07 mengj 2006-03-07 Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.
2006-02-09 paulson 2006-02-09 tidying
2006-01-31 paulson 2006-01-31 reorganization of code to support DFG otuput
2006-01-27 paulson 2006-01-27 tidying up SPASS output
2006-01-23 paulson 2006-01-23 ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-17 paulson 2006-01-17 improved SPASS support