src/HOL/Tools/ATP/atp_proof_reconstruct.ML
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
Sun, 15 Dec 2013 18:54:26 +0100 blanchet tuning
Tue, 19 Nov 2013 22:20:01 +0100 blanchet whitespace tuning
Tue, 19 Nov 2013 19:42:30 +0100 blanchet tuning
Tue, 19 Nov 2013 19:36:24 +0100 blanchet more refactoring to accommodate SMT proofs
Tue, 19 Nov 2013 18:11:52 +0100 blanchet simplified old code
Tue, 19 Nov 2013 17:37:35 +0100 blanchet refactoring
Tue, 19 Nov 2013 17:12:58 +0100 blanchet refactoring
Thu, 12 Sep 2013 22:10:57 +0200 blanchet prefixed types and some functions with "atp_" for disambiguation
Mon, 29 Jul 2013 18:06:39 +0200 blanchet avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
less more (0) -15 tip