src/HOL/TPTP/ATP_Problem_Import.thy
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-27 wenzelm 2013-06-27 manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-27 blanchet 2012-04-27 use Nitpick as an oracle for finite problems
2012-04-27 blanchet 2012-04-27 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
2012-04-27 blanchet 2012-04-27 move file to where it belongs
2012-04-27 blanchet 2012-04-27 tuning
2012-04-27 blanchet 2012-04-27 more tweaking of TPTP/CASC setup
2012-04-25 blanchet 2012-04-25 tuning
2012-04-25 blanchet 2012-04-25 more work on TPTP Isabelle and Sledgehammer tactics
2012-04-25 blanchet 2012-04-25 more work on CASC setup
2012-04-24 blanchet 2012-04-24 get rid of old parser, hopefully for good
2012-04-22 blanchet 2012-04-22 added timeout argument to TPTP tools
2012-04-18 blanchet 2012-04-18 started integrating Nik's parser into TPTP command-line tools
2012-01-23 blanchet 2012-01-23 added problem importer