src/HOL/Tools/ATP/atp_proof_reconstruct.ML
Thu, 19 Dec 2013 17:11:54 +0100 blanchet pick up tfree/tvar type from SPASS-Pirate proof
Thu, 19 Dec 2013 16:11:20 +0100 blanchet tuning
Thu, 19 Dec 2013 15:47:17 +0100 blanchet extended ATP types with sorts
Thu, 19 Dec 2013 15:04:21 +0100 blanchet removed debugging output
Thu, 19 Dec 2013 14:57:21 +0100 blanchet honor SPASS-Pirate type arguments
Wed, 18 Dec 2013 22:55:20 +0100 blanchet parse SPASS-Pirate types
Wed, 18 Dec 2013 16:50:14 +0100 blanchet tuning
Tue, 17 Dec 2013 14:15:23 +0100 blanchet tuning
Tue, 17 Dec 2013 14:03:29 +0100 blanchet primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
Tue, 17 Dec 2013 09:42:38 +0100 blanchet made SML/NJ happier
Mon, 16 Dec 2013 23:05:16 +0100 blanchet handle Skolems gracefully for SPASS as well
Mon, 16 Dec 2013 20:24:13 +0100 blanchet reverse Skolem function arguments
Mon, 16 Dec 2013 17:18:52 +0100 blanchet fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
Sun, 15 Dec 2013 19:01:06 +0100 blanchet use 'prop' rather than 'bool' systematically in Isar reconstruction code
less more (0) -14 tip