isabelle: File revisions

src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML

Tue, 29 Jun 2010 13:23:13 +0200	blanchet	rename functions	file \| diff \| annotate
Tue, 29 Jun 2010 09:19:16 +0200	blanchet	move "nice names" from Metis to TPTP format	file \| diff \| annotate
Mon, 28 Jun 2010 17:32:28 +0200	blanchet	always perform "inline" skolemization, polymorphism or not, Skolem cache or not	file \| diff \| annotate
Fri, 25 Jun 2010 17:08:39 +0200	blanchet	renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer	file \| diff \| annotate
Fri, 25 Jun 2010 16:42:06 +0200	blanchet	merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME	file \| diff \| annotate
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	file \| diff \| annotate
Wed, 23 Jun 2010 15:35:18 +0200	blanchet	renamed for easier grep	file \| diff \| annotate
Tue, 22 Jun 2010 23:54:02 +0200	blanchet	factor out TPTP format output into file of its own, to facilitate further changes	file \| diff \| annotate

isabelle