2010-04-15 blanchet 2010-04-15 make Sledgehammer's output more debugging friendly
2010-04-14 blanchet 2010-04-14 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
2010-03-29 blanchet 2010-03-29 added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29 blanchet 2010-03-29 make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
2010-03-29 blanchet 2010-03-29 made "theory_const" a Sledgehammer option; by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead.
2010-03-29 blanchet 2010-03-29 added "respect_no_atp" and "convergence" options to Sledgehammer; these were previously hard-coded in "sledgehammer_fact_filter.ML"
2010-03-24 blanchet 2010-03-24 added support for Sledgehammer parameters; this change goes hand in hand with f8c738abaed8
2010-03-19 blanchet 2010-03-19 move all ATP setup code into ATP_Wrapper
2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-17 blanchet 2010-03-17 renamed Sledgehammer structures
2010-03-05 wenzelm 2010-03-05 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
2010-03-04 wenzelm 2010-03-04 tuned;
2009-11-10 wenzelm 2009-11-10 Toplevel.thread provides Isar-style exception output;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-29 wenzelm 2009-10-29 unregister: eliminated unused status;
2009-10-28 wenzelm 2009-10-28 renamed raw Proof.get_goal to Proof.raw_goal;
2009-10-27 wenzelm 2009-10-27 SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;
2009-10-18 wenzelm 2009-10-18 removed disjunctive group cancellation -- provers run independently; sledgehammer: kill earlier session, and removed obsolete max_atps; tuned;
2009-10-18 wenzelm 2009-10-18 tuned;
2009-10-16 wenzelm 2009-10-16 made SML/NJ happy;
2009-10-15 wenzelm 2009-10-15 natural argument order for prover; renamed atp_problem to problem; standard naming convention for the_system;
2009-10-15 wenzelm 2009-10-15 ATP_Manager.get_prover: canonical argument order; eliminated various aliases of existing operations, notably Output channels; tuned messages; misc tuning and clarification;
2009-10-15 wenzelm 2009-10-15 eliminated extraneous wrapping of public records; tuned;
2009-10-15 wenzelm 2009-10-15 renamed functor HeapFun to Heap;
2009-10-15 wenzelm 2009-10-15 misc tuning and clarification;
2009-10-15 wenzelm 2009-10-15 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;
2009-10-14 wenzelm 2009-10-14 modernized structure names;
2009-10-03 boehmes 2009-10-03 merged
2009-10-03 boehmes 2009-10-03 re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values
2009-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
2009-10-01 nipkow 2009-10-01 made spass additional default prover
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-03 boehmes 2009-09-03 added runtime information to sledgehammer
2009-08-29 boehmes 2009-08-29 propagate theorem names, in addition to generated return message
2009-08-04 wenzelm 2009-08-04 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;