src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2012-12-12 ago tuned debugging file names
2012-12-12 ago made MaSh evaluation driver work with SMT solvers
2012-11-06 ago renamed Sledgehammer option
2012-11-02 ago several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
2012-10-18 ago tuned Isar output
2012-10-18 ago renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-18 ago refactor code
2012-10-16 ago added proof minimization code from Steffen Smolka
2012-08-14 ago fixed then-else confusion
2012-08-14 ago improved set of reconstructor methods
2012-08-14 ago warn users about unused "using" facts
2012-08-14 ago be less aggressive at kicking out chained facts
2012-08-14 ago recognize bus errors as crash
2012-08-07 ago stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
2012-08-03 ago cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
2012-07-26 ago Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
2012-07-20 ago added "learn_from_atp" command to MaSh, for patient users
2012-07-20 ago use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
2012-07-18 ago make the monomorphizer more predictable by making the cutoff independent on the number of facts
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 renamed Sledgehammer options
2012-07-18 ago rationalize relevance filter, slowing moving code from Iter to MaSh
2012-07-11 ago further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-06-26 ago renamed experimental option
2012-06-26 ago started adding polymophic SPASS output
2012-06-26 ago tuning
2012-06-18 ago less confusing error message
2012-06-06 ago killed most unsound encodings
2012-05-23 ago tuned names
2012-05-23 ago lower the monomorphization thresholds for less scalable provers
2012-05-21 ago add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
2012-05-16 ago lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
2012-05-13 ago get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
2012-04-24 ago made "split_last" more robust in the face of obscure low-level errors
2012-04-19 ago true delayed evaluation of "SPASS_VERSION" environment variable
2012-04-18 ago get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
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 continued implementation of term ordering attributes
2012-03-20 ago implement term order attribute (for experiments)
2012-03-20 ago internal renamings
2012-02-09 ago added possibility of generating KBO weights to DFG problems
2012-02-05 ago cleaned up new SPASS parsing
2012-02-04 ago made option available to users (mostly for experiments)
2012-02-03 ago optimization: slice caching in case two consecutive slices are nearly identical
2012-02-03 ago try to pass fewer options to Metis
2012-01-30 ago rename lambda translation schemes
2012-01-26 ago separate orthogonal components
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 cleanly separate each Metis encoding
2011-12-07 ago use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
2011-12-01 ago added "minimize" option for more control over automatic minimization
2011-12-01 ago renamed "slicing" to "slice"
2011-11-19 ago made SML/NJ happy
2011-11-18 ago be more silent when auto minimizing
2011-11-18 ago better threading of type encodings between Sledgehammer and "metis"
2011-11-18 ago don't propagate user-set "type_enc" or "lam_trans" to Metis calls
2011-11-18 ago don't needlessly pass "lam_lifted" option to "metis" call for SMT proof