src/HOL/Tools/res_atp.ML
Wed, 14 Dec 2005 16:13:09 +0100 paulson removed unused function repeat_RS
Mon, 28 Nov 2005 07:12:01 +0100 mengj Only output arities and class relations if !ResClause.keep_types is true.
Fri, 28 Oct 2005 02:29:01 +0200 mengj Added "writeln_strs" to the signature
Tue, 18 Oct 2005 15:08:38 +0200 paulson new interface to make_conjecture_clauses
Fri, 14 Oct 2005 15:34:56 +0200 paulson signature changes
Fri, 14 Oct 2005 10:19:50 +0200 paulson deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
Mon, 10 Oct 2005 15:35:29 +0200 paulson small tidy-up of utility functions
Fri, 07 Oct 2005 17:57:21 +0200 paulson minor code tidyig
Fri, 07 Oct 2005 11:29:24 +0200 paulson more tidying. Fixed process management bugs and race condition
Thu, 06 Oct 2005 10:14:22 +0200 paulson major simplification: removal of the goalstring argument
Wed, 05 Oct 2005 11:18:06 +0200 paulson improved process handling. tidied
Tue, 04 Oct 2005 09:59:01 +0200 paulson fixed the ascii-armouring of goalstring
Thu, 29 Sep 2005 12:45:04 +0200 paulson improvements for problem generation
Wed, 28 Sep 2005 11:16:27 +0200 paulson time limit option; fixed bug concerning first line of ATP output
Tue, 20 Sep 2005 18:43:39 +0200 paulson tidying, and support for axclass/classrel clauses
Tue, 20 Sep 2005 13:17:55 +0200 paulson further tidying; killing of old Watcher loops
Mon, 19 Sep 2005 18:30:22 +0200 paulson further simplification of the Isabelle-ATP linkup
Mon, 19 Sep 2005 15:12:13 +0200 paulson simplification of the Isabelle-ATP code; hooks for batch generation of problems
Fri, 16 Sep 2005 11:39:09 +0200 paulson PARTIAL conversion to Vampire8
Thu, 15 Sep 2005 17:46:00 +0200 paulson massive tidy-up and simplification
Thu, 15 Sep 2005 11:15:52 +0200 paulson the experimental tagging system, and the usual tidying
Fri, 09 Sep 2005 17:47:37 +0200 paulson Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
Wed, 07 Sep 2005 18:14:26 +0200 paulson Progress on eprover linkup, also massive tidying
Wed, 07 Sep 2005 09:54:31 +0200 paulson axioms now included in tptp files, no /bin/cat and various tidying
Fri, 02 Sep 2005 21:29:33 +0200 quigley Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
Fri, 02 Sep 2005 17:55:24 +0200 paulson further tidying up of Isabelle-ATP link
Fri, 02 Sep 2005 15:25:44 +0200 paulson tidying up the Isabelle/ATP interface
Fri, 26 Aug 2005 19:36:07 +0200 quigley DFG output now works for untyped rules (ML "ResClause.untyped();")
Wed, 17 Aug 2005 13:52:53 +0200 paulson new command to invoke ATPs
Thu, 28 Jul 2005 17:55:39 +0200 paulson dead code
Wed, 27 Jul 2005 11:30:34 +0200 paulson simpler variable names, and no types for monomorphic constants
Fri, 22 Jul 2005 17:42:40 +0200 paulson tidied up the tracing output
Wed, 20 Jul 2005 17:00:28 +0200 paulson code streamlining
Wed, 13 Jul 2005 16:07:23 +0200 wenzelm use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
Mon, 11 Jul 2005 16:42:42 +0200 quigley Fixed some problems with the signal handler.
Thu, 07 Jul 2005 18:25:02 +0200 paulson inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
Mon, 04 Jul 2005 15:51:56 +0200 quigley Streamlined the signal handler in watcher.ML
Tue, 21 Jun 2005 23:44:18 +0200 quigley Integrated vampire lemma code.
Tue, 21 Jun 2005 13:34:24 +0200 paulson VAMPIRE_HOME, helper_path and various stylistic tweaks
Mon, 20 Jun 2005 18:39:24 +0200 quigley Added VampCommunication.ML.
Mon, 20 Jun 2005 15:55:44 +0200 paulson using TPTP2X_HOME; indentation, etc
Fri, 10 Jun 2005 16:15:36 +0200 quigley All subgoals sent to the watcher at once now.
Sun, 05 Jun 2005 11:31:22 +0200 wenzelm File.platform_path;
Thu, 02 Jun 2005 15:54:11 +0200 quigley Added time lime (60 secs) to Spass calls.
Wed, 01 Jun 2005 14:50:48 +0200 paulson small tweaks; also now write_out_clasimp takes the current theory as argument
Tue, 31 May 2005 12:42:36 +0200 quigley Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
Thu, 26 May 2005 16:50:07 +0200 paulson trying to set up portable calling sequences for SPASS and tptp2X
Tue, 24 May 2005 10:23:24 +0200 paulson A new structure and reduced indentation
Mon, 23 May 2005 00:18:51 +0200 quigley Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
Tue, 03 May 2005 14:27:21 +0200 quigley Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
Wed, 20 Apr 2005 18:01:50 +0200 quigley Corrected the problem with the ATP directory.
Wed, 20 Apr 2005 16:03:17 +0200 quigley Removed remaining references to Main.thy in reconstruction code.
Tue, 19 Apr 2005 18:08:44 +0200 paulson more tidying of libraries in Reconstruction
Fri, 15 Apr 2005 13:35:53 +0200 paulson more tidying up of the SPASS interface
Tue, 12 Apr 2005 11:08:25 +0200 paulson tweaks mainly to achieve sml/nj compatibility
Mon, 11 Apr 2005 16:25:31 +0200 paulson removal of Main and other tidying up
Thu, 07 Apr 2005 18:44:45 +0200 paulson removed bad code
Thu, 07 Apr 2005 18:20:04 +0200 quigley Integrating the reconstruction files into the building of HOL
Tue, 05 Apr 2005 16:32:47 +0200 quigley Current version of res_atp.ML - causes an error when I run it. C.Q.
Mon, 04 Apr 2005 18:43:18 +0200 quigley Updated to add watcher code.
less more (0) -60 tip