src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2010-06-22 ago removed Sledgehammer's support for the DFG syntax;
2010-06-11 ago proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-05 ago totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
2010-06-04 ago made "clausify" attribute a legacy feature;
2010-06-04 ago made "neg_clausify" a legacy feature
2010-06-04 ago kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
2010-05-28 ago make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-14 ago renamed options
2010-05-14 ago renamed two Sledgehammer options
2010-05-14 ago delect installed ATPs dynamically, _not_ at image built time
2010-05-01 ago made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-04-28 ago remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
2010-04-27 ago make Sledgehammer more friendly if no subgoal is left
2010-04-27 ago remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
2010-04-26 ago rename options
2010-04-25 ago cosmetics
2010-04-25 ago move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-23 ago remove some bloat
2010-04-23 ago renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23 ago move the minimizer to the Sledgehammer directory
2010-04-23 ago move some sledgehammer stuff out of "atp_manager.ML"
2010-04-23 ago move the Sledgehammer menu options to "sledgehammer_isar.ML"
2010-04-22 ago remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
2010-04-21 ago pass relevant options from "sledgehammer" to "sledgehammer minimize";
2010-04-20 ago 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 ago make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19 ago rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-16 ago by default, don't try to start ATPs that aren't installed
2010-04-16 ago fiddle with Sledgehammer option syntax
2010-04-16 ago Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-14 ago added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
2010-04-14 ago make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-04-14 ago make Sledgehammer's "timeout" option work for "minimize"
2010-04-14 ago fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
2010-03-29 ago added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29 ago make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
2010-03-29 ago made "theory_const" a Sledgehammer option;
2010-03-29 ago added "respect_no_atp" and "convergence" options to Sledgehammer;
2010-03-28 ago make SML/NJ happy
2010-03-25 ago make Mirabelle happy again
2010-03-24 ago revert debugging output that shouldn't have been submitted in the first place
2010-03-24 ago honor the newly introduced Sledgehammer parameters and fixed the parsing;
2010-03-23 ago added a syntax for specifying facts to Sledgehammer;
2010-03-23 ago added options to Sledgehammer;
2010-03-22 ago make "sledgehammer" and "atp_minimize" improper commands
2010-03-19 ago move the Sledgehammer Isar commands together into one file;