src/HOL/Tools/ATP/atp_proof.ML
2010-11-24 blanchet 2010-11-24 more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
2010-11-23 blanchet 2010-11-23 more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-15 blanchet 2010-11-15 pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-09-23 blanchet 2010-09-23 make SML/NJ happy
2010-09-22 blanchet 2010-09-22 make SML/NJ happier
2010-09-21 blanchet 2010-09-21 make SML/NJ happier
2010-09-16 blanchet 2010-09-16 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
2010-09-16 blanchet 2010-09-16 avoid code duplication
2010-09-16 blanchet 2010-09-16 merge constructors
2010-09-16 blanchet 2010-09-16 factor out the inverse of "nice_atp_problem"
2010-09-16 blanchet 2010-09-16 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
2010-09-16 blanchet 2010-09-16 factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"