src/HOL/Tools/res_atp.ML
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-12 wenzelm 2008-06-12 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-16 wenzelm 2008-04-16 valid_facts: more elementary version using Facts.fold_static;
2008-04-15 wenzelm 2008-04-15 all_valid_thms: use new facts tables;
2008-04-15 wenzelm 2008-04-15 Facts.dest_table;
2008-03-31 wenzelm 2008-03-31 discontinued File.explode_platform_path -- use plain Path.explode;
2008-03-15 wenzelm 2008-03-15 replaced obsolete FactIndex.T by Facts.T;
2008-01-02 paulson 2008-01-02 testing for empty sort
2007-11-28 paulson 2007-11-28 Chained theorems are no longer mentioned in metis calls and (if used) they prevent the output of a structured proof.
2007-10-30 paulson 2007-10-30 bugfixes concerning strange theorems
2007-10-18 paulson 2007-10-18 Ensured that the right number of ATP calls is generated
2007-10-16 paulson 2007-10-16 added the "max_sledgehammers" option
2007-10-12 paulson 2007-10-12 calling the correct interface
2007-10-11 paulson 2007-10-11 rationalized redundant code
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 paulson 2007-10-05 filtering out some package theorems
2007-10-04 paulson 2007-10-04 combinator translation
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;
2007-09-06 paulson 2007-09-06 chained facts are now included
2007-08-24 paulson 2007-08-24 Returning both a "one-line" proof and a structured proof
2007-08-18 wenzelm 2007-08-18 removed obsolete atp_method; ResHolClause.XXX_write_file: theory argument;
2007-08-17 wenzelm 2007-08-17 proper signature for Meson;
2007-08-15 paulson 2007-08-15 combining the relevance filter with res_atp
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);