src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2012-01-19 blanchet 2012-01-19 renamed "sound" option to "strict"
2012-01-19 blanchet 2012-01-19 cleanly separate each Metis encoding
2011-12-07 blanchet 2011-12-07 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 blanchet 2011-12-01 added "minimize" option for more control over automatic minimization
2011-12-01 blanchet 2011-12-01 renamed "slicing" to "slice"
2011-11-19 blanchet 2011-11-19 made SML/NJ happy
2011-11-18 blanchet 2011-11-18 be more silent when auto minimizing
2011-11-18 blanchet 2011-11-18 better threading of type encodings between Sledgehammer and "metis"
2011-11-18 blanchet 2011-11-18 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
2011-11-18 blanchet 2011-11-18 don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
2011-11-18 blanchet 2011-11-18 quiet down SMT
2011-11-18 blanchet 2011-11-18 more aggressive lambda hiding (if we anyway need to pass an option to Metis)
2011-11-18 blanchet 2011-11-18 don't pass "lam_lifted" option to "metis" unless there's a good reason
2011-11-18 blanchet 2011-11-18 no needless reconstructors
2011-11-18 blanchet 2011-11-18 removed more clutter
2011-11-18 blanchet 2011-11-18 removed needless baggage
2011-11-16 blanchet 2011-11-16 give each time slice its own lambda translation
2011-11-16 blanchet 2011-11-16 thread in additional options to minimizer
2011-11-16 blanchet 2011-11-16 make metis reconstruction handling more flexible
2011-11-16 blanchet 2011-11-16 parse lambda translation option in Metis
2011-11-15 blanchet 2011-11-15 rename configuration option to more reasonable length
2011-11-15 blanchet 2011-11-15 started implementing lambda-lifting in Metis
2011-11-06 blanchet 2011-11-06 more millisecond cleanup
2011-11-06 blanchet 2011-11-06 try "smt" as a fallback for ATPs if "metis" fails/times out
2011-11-06 blanchet 2011-11-06 more detailed preplay output
2011-11-06 blanchet 2011-11-06 tuning
2011-11-06 blanchet 2011-11-06 use "Time.time" rather than milliseconds internally
2011-11-06 blanchet 2011-11-06 tune: no need for option
2011-10-29 blanchet 2011-10-29 added DFG unsorted support (like in the old days)
2011-10-29 blanchet 2011-10-29 added sorted DFG output for coming version of SPASS
2011-10-29 blanchet 2011-10-29 check "sound" flag before doing something unsound...
2011-09-13 blanchet 2011-09-13 simplified unsound proof detection by removing impossible case
2011-09-10 blanchet 2011-09-10 continue with minimization in debug mode in spite of unsoundness
2011-09-02 blanchet 2011-09-02 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-09-02 blanchet 2011-09-02 fewer TPTP important messages
2011-09-01 blanchet 2011-09-01 always measure time for ATPs -- auto minimization relies on it
2011-09-01 blanchet 2011-09-01 make "sound" sound and "unsound" more sound, based on evaluation
2011-08-30 blanchet 2011-08-30 fixed just introduced silly bug
2011-08-30 blanchet 2011-08-30 tuning
2011-08-30 blanchet 2011-08-30 flip logic of boolean option so it's off by default
2011-08-30 nik 2011-08-30 improved handling of induction rules in Sledgehammer
2011-08-30 nik 2011-08-30 added generation of induction rules
2011-08-26 blanchet 2011-08-26 added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
2011-08-23 blanchet 2011-08-23 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23 blanchet 2011-08-23 added formats to the slice and use TFF for remote Vampire
2011-08-22 blanchet 2011-08-22 cleaner handling of polymorphic monotonicity inference
2011-08-22 blanchet 2011-08-22 added option to control soundness of encodings more precisely, for evaluation purposes
2011-08-22 blanchet 2011-08-22 make sound mode more sound (and clean up code)
2011-08-09 blanchet 2011-08-09 move lambda-lifting code to ATP encoding, so it can be used by Metis
2011-07-28 blanchet 2011-07-28 tuning
2011-07-26 blanchet 2011-07-26 remove spurious message
2011-07-25 blanchet 2011-07-25 introduced hybrid lambda translation
2011-07-25 blanchet 2011-07-25 avoid needless type args for lifted-lambdas
2011-07-21 blanchet 2011-07-21 make "concealed" lambda translation sound
2011-07-20 blanchet 2011-07-20 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
2011-07-20 boehmes 2011-07-20 generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
2011-07-20 boehmes 2011-07-20 moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
2011-07-17 blanchet 2011-07-17 fixed lambda-liftg: must ensure the formulas are in close form
2011-07-17 blanchet 2011-07-17 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)