src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
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-04-14 blanchet 2010-04-14 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-04-14 blanchet 2010-04-14 make Sledgehammer's "timeout" option work for "minimize"
2010-04-14 blanchet 2010-04-14 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"
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-28 blanchet 2010-03-28 make SML/NJ happy
2010-03-25 blanchet 2010-03-25 make Mirabelle happy again
2010-03-24 blanchet 2010-03-24 revert debugging output that shouldn't have been submitted in the first place
2010-03-24 blanchet 2010-03-24 honor the newly introduced Sledgehammer parameters and fixed the parsing; e.g. the prover "e_isar" (formely "e_full") is gone, instead do sledgehammer [atps = e, isar_proof] to get the same effect
2010-03-23 blanchet 2010-03-23 added a syntax for specifying facts to Sledgehammer; e.g., sledgehammer (add: foo del: bar) which tells the relevance filter to include "foo" but omit "bar".
2010-03-23 blanchet 2010-03-23 added options to Sledgehammer; syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
2010-03-22 blanchet 2010-03-22 make "sledgehammer" and "atp_minimize" improper commands
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