src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-07-29 blanchet 2010-07-29 use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses
2010-07-28 blanchet 2010-07-28 minor refactoring
2010-07-28 blanchet 2010-07-28 minor refactoring
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-06-28 blanchet 2010-06-28 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
2010-06-28 blanchet 2010-06-28 always perform relevance filtering on original formulas
2010-06-25 blanchet 2010-06-25 factor out thread creation
2010-06-25 blanchet 2010-06-25 got rid of "respect_no_atp" option, which even I don't use
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-25 blanchet 2010-06-25 further reduce dependencies on "sledgehammer_fact_filter.ML"
2010-06-23 blanchet 2010-06-23 killed legacy "neg_clausify" and "clausify"
2010-06-22 blanchet 2010-06-22 removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-05 blanchet 2010-06-05 totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax; faster and more reliable
2010-06-04 blanchet 2010-06-04 made "clausify" attribute a legacy feature; seems to have ever only been a debugging feature
2010-06-04 blanchet 2010-06-04 made "neg_clausify" a legacy feature
2010-06-04 blanchet 2010-06-04 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
2010-05-28 blanchet 2010-05-28 make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-14 blanchet 2010-05-14 renamed options
2010-05-14 blanchet 2010-05-14 renamed two Sledgehammer options
2010-05-14 blanchet 2010-05-14 delect installed ATPs dynamically, _not_ at image built time
2010-05-01 krauss 2010-05-01 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-04-28 blanchet 2010-04-28 remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; what we need is smarter type annotations for variables _and_ constants
2010-04-27 blanchet 2010-04-27 make Sledgehammer more friendly if no subgoal is left
2010-04-27 blanchet 2010-04-27 remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-26 blanchet 2010-04-26 rename options
2010-04-25 blanchet 2010-04-25 cosmetics
2010-04-25 blanchet 2010-04-25 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-23 blanchet 2010-04-23 remove some bloat
2010-04-23 blanchet 2010-04-23 renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23 blanchet 2010-04-23 move the minimizer to the Sledgehammer directory
2010-04-23 blanchet 2010-04-23 move some sledgehammer stuff out of "atp_manager.ML"
2010-04-23 blanchet 2010-04-23 move the Sledgehammer menu options to "sledgehammer_isar.ML"
2010-04-22 blanchet 2010-04-22 remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
2010-04-21 blanchet 2010-04-21 pass relevant options from "sledgehammer" to "sledgehammer minimize"; one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files
2010-04-20 blanchet 2010-04-20 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-19 blanchet 2010-04-19 make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19 blanchet 2010-04-19 rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-16 blanchet 2010-04-16 by default, don't try to start ATPs that aren't installed
2010-04-16 blanchet 2010-04-16 fiddle with Sledgehammer option syntax
2010-04-16 blanchet 2010-04-16 Sledgehammer: the empty set of fact () should mean nothing, not unchanged
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