src/HOL/Tools/res_atp.ML
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Wed, 30 Sep 2009 11:33:59 +0200 Philipp Meyer atp_minimal using chain_ths again
Thu, 10 Sep 2009 16:16:18 +0200 Philipp Meyer atp_minimize is now not using whitelist
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Thu, 09 Jul 2009 22:01:41 +0200 wenzelm renamed functor TableFun to Table, and GraphFun to Graph;
Thu, 02 Jul 2009 10:49:46 +0100 paulson Deleted some debugging code
Tue, 30 Jun 2009 11:21:02 +0200 immler fixed: count constants with supplementary lemmas
Sun, 28 Jun 2009 15:01:28 +0200 immler whitelist for HOL problems with ext:
Sun, 28 Jun 2009 15:01:28 +0200 immler always include whitelist;
Mon, 22 Jun 2009 17:07:09 +0200 immler use results of relevance-filter to determine additional clauses;
Mon, 22 Jun 2009 17:07:08 +0200 immler corrected comments
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Wed, 03 Jun 2009 16:56:41 +0200 immler include chain-ths in every prover-call
Wed, 03 Jun 2009 16:56:41 +0200 immler split preparing clauses and writing problemfile;
Sat, 14 Mar 2009 16:46:23 +0100 immler split relevance-filter and writing of problem-files;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 21:06:59 +0100 wenzelm removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Thu, 26 Feb 2009 10:13:43 +0100 immler removed global ref dfg_format
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm use exists_subterm directly;
Fri, 03 Oct 2008 16:37:09 +0200 wenzelm version of sledgehammer using threads instead of processes, misc cleanup;
Mon, 01 Sep 2008 10:19:38 +0200 nipkow Prover is set via menu now
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Thu, 12 Jun 2008 18:54:29 +0200 wenzelm ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Wed, 16 Apr 2008 21:52:59 +0200 wenzelm valid_facts: more elementary version using Facts.fold_static;
Tue, 15 Apr 2008 22:09:23 +0200 wenzelm all_valid_thms: use new facts tables;
Tue, 15 Apr 2008 18:49:15 +0200 wenzelm Facts.dest_table;
Mon, 31 Mar 2008 23:08:51 +0200 wenzelm discontinued File.explode_platform_path -- use plain Path.explode;
Sat, 15 Mar 2008 18:07:59 +0100 wenzelm replaced obsolete FactIndex.T by Facts.T;
Wed, 02 Jan 2008 12:22:38 +0100 paulson testing for empty sort
Wed, 28 Nov 2007 16:26:03 +0100 paulson Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
Tue, 30 Oct 2007 15:28:53 +0100 paulson bugfixes concerning strange theorems
Thu, 18 Oct 2007 17:33:57 +0200 paulson Ensured that the right number of ATP calls is generated
Tue, 16 Oct 2007 16:18:36 +0200 paulson added the "max_sledgehammers" option
Fri, 12 Oct 2007 15:45:13 +0200 paulson calling the correct interface
Thu, 11 Oct 2007 15:59:31 +0200 paulson rationalized redundant code
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Fri, 05 Oct 2007 09:59:03 +0200 paulson filtering out some package theorems
Thu, 04 Oct 2007 12:32:58 +0200 paulson combinator translation
Tue, 18 Sep 2007 18:05:37 +0200 wenzelm simplified PrintMode interfaces;
Mon, 17 Sep 2007 16:36:41 +0200 wenzelm avoid direct access to print_mode;
Thu, 06 Sep 2007 17:03:32 +0200 paulson chained facts are now included
Fri, 24 Aug 2007 14:16:44 +0200 paulson Returning both a "one-line" proof and a structured proof
Sat, 18 Aug 2007 13:32:21 +0200 wenzelm removed obsolete atp_method;
Fri, 17 Aug 2007 00:03:50 +0200 wenzelm proper signature for Meson;
Wed, 15 Aug 2007 13:50:47 +0200 paulson combining the relevance filter with res_atp
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Fri, 10 Aug 2007 15:13:18 +0200 paulson removal of some refs
Thu, 14 Jun 2007 13:19:50 +0200 paulson Now ResHolClause also does first-order problems!
Thu, 17 May 2007 13:37:24 +0200 paulson Added three items to the signature
Tue, 08 May 2007 15:01:30 +0200 wenzelm renamed call_atp to sledgehammer;
Mon, 30 Apr 2007 13:22:15 +0200 paulson Removal of dead code
Thu, 19 Apr 2007 18:23:11 +0200 paulson trying to make single-step proofs work better, especially if they contain
Wed, 18 Apr 2007 11:14:09 +0200 paulson Fixes for proof reconstruction, especially involving abstractions and definitions
less more (0) -100 -60 tip