src/HOL/Tools/ATP/res_clasimpset.ML
Wed, 20 Jul 2005 17:00:28 +0200 paulson code streamlining
Wed, 13 Jul 2005 15:06:04 +0200 paulson relevance filtering is now optional
Thu, 07 Jul 2005 18:25:02 +0200 paulson inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
Fri, 10 Jun 2005 16:15:36 +0200 quigley All subgoals sent to the watcher at once now.
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
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.
Thu, 12 May 2005 18:24:42 +0200 paulson theorem names for caching
Tue, 03 May 2005 14:27:21 +0200 quigley Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
Mon, 02 May 2005 13:30:48 +0200 paulson deleted redundant code
Thu, 28 Apr 2005 17:56:58 +0200 paulson fixed treatment of higher-order simprules
Thu, 21 Apr 2005 15:05:24 +0200 paulson added hearder lines and deleted some redundant material
Wed, 20 Apr 2005 18:01:50 +0200 quigley Corrected the problem with the ATP directory.
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
Thu, 31 Mar 2005 19:47:30 +0200 quigley *** empty log message ***
less more (0) tip