src/HOL/Tools/ATP/atp_proof.ML
Wed, 08 Dec 2010 22:17:53 +0100 blanchet reword error message
Wed, 24 Nov 2010 16:15:15 +0100 blanchet more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
Tue, 23 Nov 2010 22:37:16 +0100 blanchet more precise error handling for Z3;
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Mon, 15 Nov 2010 18:56:29 +0100 blanchet pick up SMT solver crashes and report them to the user/Mirabelle if desired
Thu, 23 Sep 2010 10:34:01 +0200 blanchet make SML/NJ happy
Wed, 22 Sep 2010 10:02:39 +0200 blanchet make SML/NJ happier
Tue, 21 Sep 2010 10:02:50 +0200 blanchet make SML/NJ happier
Thu, 16 Sep 2010 15:16:08 +0200 blanchet refactoring: move ATP proof and error extraction code to "ATP_Proof" module
Thu, 16 Sep 2010 14:24:48 +0200 blanchet avoid code duplication
Thu, 16 Sep 2010 13:52:17 +0200 blanchet merge constructors
Thu, 16 Sep 2010 13:44:41 +0200 blanchet factor out the inverse of "nice_atp_problem"
Thu, 16 Sep 2010 11:59:45 +0200 blanchet use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
Thu, 16 Sep 2010 11:12:08 +0200 blanchet factored out TSTP/SPASS/Vampire proof parsing;
less more (0) tip