src/HOL/Tools/res_atp.ML
2006-10-10 ago A way to call the ATP linkup from ML scripts
2006-10-06 ago Tidied code to delete tmp files.
2006-10-06 ago Improved detection of identical clauses, also in the conjecture
2006-10-04 ago insert replacing ins ins_int ins_string
2006-10-02 ago restored the "length of name > 2" check for package definitions
2006-09-29 ago simplified is_package_def -- be less ambitious about B library operations;
2006-09-28 ago Definitions produced by packages are now blacklisted.
2006-09-21 ago Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
2006-09-20 ago Removed include_min_comb and include_combS.
2006-09-14 ago made SML/NJ happy;
2006-09-13 ago Extended the blacklist with higher-order theorems. Restructured. Added checks to
2006-09-01 ago refinements to conversion into clause form, esp for the HO case
2006-08-31 ago String.concatWith (not available in PolyML) replaced by space_implode
2006-08-31 ago blacklist now handles thm lists
2006-08-28 ago minor bug fixes
2006-08-25 ago abstraction of lambda-expressions
2006-08-09 ago blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-28 ago "all theorems" mode forces definition-expansion off.
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-15 ago Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
2006-07-06 ago some tidying; fixed the output of theorem names
2006-06-15 ago the "all_theorems" option and some fixes
2006-06-04 ago ATP/res_clasimpset.ML has been merged into res_atp.ML.
2006-05-29 ago warnings to debug outputs
2006-05-29 ago Giving the "--silent" switch to E, to produce less output
2006-05-25 ago Added in settings used by "spass" method.
2006-05-25 ago Added support for DFG format, used by SPASS.
2006-05-17 ago removing the string array from the result of get_clasimp_atp_lemmas
2006-05-16 ago replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
2006-05-11 ago avoid raw equality on type thm;
2006-04-28 ago removed the functions for getting HOL helper paths.
2006-04-20 ago Changed the logic detection method.
2006-04-19 ago exported linkup_logic_mode and changed the default setting
2006-04-19 ago tidying; ATP options including CASC mode for Vampire
2006-04-18 ago Tidied up some programs.
2006-04-07 ago lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
2006-03-09 ago Added more functions to the signature and tidied up some functions.
2006-03-07 ago Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
2006-03-07 ago Merged res_atp_setup.ML into res_atp.ML.
2006-02-09 ago tidying
2006-01-31 ago reorganization of code to support DFG otuput
2006-01-27 ago tidying up SPASS output
2006-01-23 ago ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-17 ago improved SPASS support
2006-01-14 ago Output.debug;
2006-01-13 ago more practical time limit
2005-12-14 ago removed unused function repeat_RS
2005-11-28 ago Only output arities and class relations if !ResClause.keep_types is true.
2005-10-28 ago Added "writeln_strs" to the signature
2005-10-18 ago new interface to make_conjecture_clauses
2005-10-14 ago signature changes
2005-10-14 ago deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-10 ago small tidy-up of utility functions
2005-10-07 ago minor code tidyig
2005-10-07 ago more tidying. Fixed process management bugs and race condition
2005-10-06 ago major simplification: removal of the goalstring argument
2005-10-05 ago improved process handling. tidied
2005-10-04 ago fixed the ascii-armouring of goalstring
2005-09-29 ago improvements for problem generation