src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2012-12-12 ago adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
2012-11-12 ago create temp directory if not already created
2012-11-06 ago renamed Sledgehammer option
2012-10-18 ago renamed Isar-proof related options + changed semantics of Isar shrinking
2012-09-28 ago tuned message
2012-09-14 ago merged two commands
2012-07-26 ago detect unknown options again
2012-07-23 ago don't relearn old facts in Isar mode
2012-07-23 ago took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
2012-07-20 ago honor suggested MaSh weights
2012-07-20 ago use CVC3 and Yices by default if they are available and there are enough cores
2012-07-20 ago minimal maxes + tuning
2012-07-20 ago learn from SMT proofs when they can be minimized by Metis
2012-07-20 ago convenience
2012-07-20 ago learning should honor the fact override and the chained facts
2012-07-20 ago added "learn_from_atp" command to MaSh, for patient users
2012-07-20 ago more MaSh docs
2012-07-20 ago learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
2012-07-20 ago learn command in MaSh
2012-07-20 ago renamed ML structures
2012-07-18 ago optimize parent computation in MaSh + remove temporary files
2012-07-18 ago learn from minimized ATP proofs
2012-07-18 ago use async manager to manage MaSh learners to make sure they get killed cleanly
2012-07-18 ago added option to control which fact filter is used
2012-07-18 ago make tracing an option
2012-07-18 ago more implementation work on MaSh
2012-07-18 ago started implementing MaSh client-side I/O
2012-07-18 ago renamed Sledgehammer options
2012-07-18 ago more code rationalization in relevance filter
2012-07-11 ago further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-05-23 ago lower the monomorphization thresholds for less scalable provers
2012-04-21 ago swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
2012-03-21 ago improve "remote_satallax" by exploiting unsat core
2012-03-20 ago made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
2012-03-20 ago added "dont_preplay" alias
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 ago prefer formally checked @{keyword} parser;
2012-02-06 ago renamed type encoding
2012-02-04 ago made option available to users (mostly for experiments)
2012-02-02 ago include new SPASS by default if available
2012-01-23 ago renamed two files to make room for a new file
2012-01-19 ago renamed "sound" option to "strict"
2012-01-19 ago lower timeout for preplay, now that we have more preplay methods
2011-12-01 ago added "minimize" option for more control over automatic minimization
2011-12-01 ago renamed "slicing" to "slice"
2011-11-16 ago thread in additional options to minimizer
2011-11-16 ago make metis reconstruction handling more flexible
2011-11-16 ago parse lambda translation option in Metis
2011-09-23 ago reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
2011-09-22 ago take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
2011-09-07 ago parse new experimental '@' encodings
2011-09-07 ago tuning
2011-09-07 ago rationalize uniform encodings
2011-09-05 ago fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
2011-09-02 ago renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-08-30 ago extended simple types with polymorphism -- the implementation still needs some work though
2011-08-25 ago rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-24 ago more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-22 ago cleaner handling of polymorphic monotonicity inference
2011-08-09 ago renamed E wrappers for consistency with CASC conventions