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;
2009-11-06 nipkow 2009-11-06 Command atp_minimize uses the naive linear algorithm now because the binary chop one had turned out to be a little bit suboptimal. Internally the binary chop one is still available.
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-29 wenzelm 2009-10-29 tuned;
2009-10-28 wenzelm 2009-10-28 renamed raw Proof.get_goal to Proof.raw_goal;
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 misc tuning and recovery of Isabelle coding style;
2009-10-15 wenzelm 2009-10-15 eliminated extraneous wrapping of public records; tuned;
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 re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-14 nipkow 2009-09-14 count number of iterations required for minimization (and fixed bug: minimization was always called)
2009-09-07 nipkow 2009-09-07 Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
2009-09-05 boehmes 2009-09-05 added signature ATP_MINIMAL, fixed AtpMinimal.minimalize for the trivial case, Mirabelle: added an option to minimize a theorem set found by sledgehammer, use timeout of sledgehammer instead of additional timeLimit
2009-09-03 boehmes 2009-09-03 added runtime information to sledgehammer
2009-08-04 wenzelm 2009-08-04 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;