2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-02 paulson 2009-07-02 Deleted some debugging code
2009-06-30 immler 2009-06-30 fixed: count constants with supplementary lemmas
2009-06-28 immler 2009-06-28 whitelist for HOL problems with ext: as a 'helper clause' ext was not passed to metis, but metis does not include ext
2009-06-28 immler 2009-06-28 always include whitelist;
2009-06-22 immler 2009-06-22 use results of relevance-filter to determine additional clauses; (needed for minimize to be able to prove the same problems as sledgehammer)
2009-06-22 immler 2009-06-22 corrected comments
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-03 immler 2009-06-03 include chain-ths in every prover-call
2009-06-03 immler 2009-06-03 split preparing clauses and writing problemfile; included results of count_constants in return-type of prover; optionally pass counted constants to prover; removed unused external_prover from signature
2009-03-14 immler 2009-03-14 split relevance-filter and writing of problem-files; perform relevance-filtering for only one subgoal; added additional explicit timeout to provers
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-26 immler 2009-02-26 removed global ref dfg_format
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 use exists_subterm directly;
2008-10-03 wenzelm 2008-10-03 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);
2008-09-01 nipkow 2008-09-01 Prover is set via menu now
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.