src/HOL/Tools/res_atp.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-20 paulson 2009-10-20 Removal of the unused atpset concept, the atp attribute and some related code.
2009-10-18 wenzelm 2009-10-18 removed some unreferenced material; tuned;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-16 wenzelm 2009-10-16 local channels for tracing/debugging;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-30 Philipp Meyer 2009-09-30 atp_minimal using chain_ths again
2009-09-10 Philipp Meyer 2009-09-10 atp_minimize is now not using whitelist
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
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