src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
Sat, 03 Jul 2010 00:49:12 +0200 blanchet remove needless signature entry
Wed, 30 Jun 2010 18:03:34 +0200 blanchet rewrote the TPTP problem generation code more or less from scratch;
Tue, 29 Jun 2010 13:23:13 +0200 blanchet rename functions
Tue, 29 Jun 2010 09:19:16 +0200 blanchet move "nice names" from Metis to TPTP format
Mon, 28 Jun 2010 17:32:28 +0200 blanchet always perform "inline" skolemization, polymorphism or not, Skolem cache or not
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
Wed, 23 Jun 2010 16:28:12 +0200 blanchet fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
Wed, 23 Jun 2010 15:35:18 +0200 blanchet renamed for easier grep
Tue, 22 Jun 2010 23:54:02 +0200 blanchet factor out TPTP format output into file of its own, to facilitate further changes
less more (0) tip