src/HOL/Tools/atp_wrapper.ML
Tue, 28 Jul 2009 18:17:35 +0200 wenzelm neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
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.;
Sun, 28 Jun 2009 15:01:29 +0200 immler check if conjectures have been used in proof
Sun, 28 Jun 2009 15:01:28 +0200 immler use structure File instead of TextIO;
Sun, 28 Jun 2009 15:01:28 +0200 immler check for current versions on server
Sun, 28 Jun 2009 15:01:28 +0200 immler fixed
Wed, 24 Jun 2009 15:51:07 +0200 nipkow New ATP option: full types
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 export proof when exporting problemfile
Mon, 22 Jun 2009 17:07:08 +0200 immler restructured external_prover
Wed, 03 Jun 2009 16:56:41 +0200 immler additional debugging
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;
Tue, 02 Jun 2009 16:52:37 +0200 wenzelm made SML/NJ happy;
Mon, 04 May 2009 23:37:39 +0200 immler added Philipp Meyer's implementation of AtpMinimal
Sat, 25 Apr 2009 20:31:27 +0200 wenzelm renamed contrib/SystemOnTPTP/remote to lib/script/SystemOnTPTP, thus leaving contrib empty within the official distribution;
Thu, 16 Apr 2009 14:54:57 +0200 wenzelm external_prover: "exec" the command line, in order to preserve the exact process context of the "system" invocation (this recovers interruptibility of E-1.0, which assumes to be the process group leader);
Wed, 15 Apr 2009 15:27:13 +0200 wenzelm more generic error message, which also covers more fundamental failure;
Sat, 04 Apr 2009 20:22:39 +0200 immler reverted to explicitly check the presence of a refutation
Mon, 16 Mar 2009 14:26:30 +0100 immler have remote script interrupted like the other provers
Sat, 14 Mar 2009 16:50:25 +0100 immler use goal instead of Proof State
Sat, 14 Mar 2009 16:46:23 +0100 immler split relevance-filter and writing of problem-files;
Sat, 14 Mar 2009 15:45:45 +0100 immler show certain errors to the user
Sat, 14 Mar 2009 15:15:44 +0100 immler removed connection check;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Thu, 26 Feb 2009 10:13:43 +0100 immler removed global ref dfg_format
Fri, 20 Feb 2009 16:48:01 +0100 immler changed message
Fri, 20 Feb 2009 11:04:18 +0100 immler detailed information on atp-failure via Output.debug
Wed, 21 Jan 2009 14:57:33 +0100 immler tuned;
Tue, 20 Jan 2009 20:58:08 +0100 immler pass timeout to prover;
Tue, 20 Jan 2009 16:05:57 +0100 immler modified remote script;
Mon, 12 Jan 2009 16:16:05 +0100 immler simplified usage of remote-script; added compatible remote-atps
Tue, 14 Oct 2008 20:10:45 +0200 wenzelm tuned interfaces -- plain prover function, without thread;
Tue, 14 Oct 2008 16:01:36 +0200 wenzelm renamed AtpThread to AtpWrapper;
less more (0) tip