2014-06-22 sultana 2014-06-22 Metis is being used to emulate E steps;
2014-06-22 sultana 2014-06-22 updated application of print_tac to take context parameter;
2014-08-02 blanchet 2014-08-02 better duplicate detection
2014-08-01 blanchet 2014-08-01 normalize conjectures vs. negated conjectures when comparing terms
2014-08-01 blanchet 2014-08-01 tweaked 'clone' formula detection
2014-08-01 blanchet 2014-08-01 fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01 blanchet 2014-08-01 centralized boolean simplification so that e.g. LEO-II benefits from it
2014-08-01 blanchet 2014-08-01 careful when compressing 'obtains'
2014-08-01 blanchet 2014-08-01 better handling of variable names
2014-08-01 blanchet 2014-08-01 try to get rid of skolems first
2014-08-01 blanchet 2014-08-01 nicer generated variable names
2014-08-01 blanchet 2014-08-01 tuning
2014-08-01 blanchet 2014-08-01 tuning
2014-08-01 blanchet 2014-08-01 no need to 'obtain' variables not in formula
2014-08-01 blanchet 2014-08-01 more precise handling of LEO-II skolemization
2014-08-01 blanchet 2014-08-01 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
2014-08-01 blanchet 2014-08-01 tuning
2014-08-01 blanchet 2014-08-01 peek instead of joining -- is perhaps less risky
2014-08-01 blanchet 2014-08-01 export ML function
2014-08-01 blanchet 2014-08-01 compile
2014-08-01 blanchet 2014-08-01 removed 'metisFT' support in Mirabelle
2014-08-01 blanchet 2014-08-01 removed Mirabelle minimization code
2014-08-01 blanchet 2014-08-01 modernized Mirabelle (a bit) and made it compile
2014-08-01 blanchet 2014-08-01 restored a bit of laziness
2014-08-01 blanchet 2014-08-01 reorder quantifiers to ease Z3 skolemization
2014-08-01 blanchet 2014-08-01 tuned order of arguments
2014-08-01 blanchet 2014-08-01 tuned name context code
2014-08-01 blanchet 2014-08-01 tuned whitespace
2014-08-01 blanchet 2014-08-01 more rational unskolemizing of names
2014-08-01 blanchet 2014-08-01 added appropriate method for skolemization of Z3 steps to the mix
2014-08-01 blanchet 2014-08-01 pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
2014-08-01 blanchet 2014-08-01 honor 'try0' also for one-liners
2014-08-01 blanchet 2014-08-01 tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01 blanchet 2014-08-01 further minimize one-liner
2014-08-01 blanchet 2014-08-01 tuning
2014-08-01 blanchet 2014-08-01 eliminated needlessly complex message tail
2014-08-01 blanchet 2014-08-01 updated NEWS
2014-08-01 blanchet 2014-08-01 update documentation after removal of 'min' subcommand
2014-08-01 blanchet 2014-08-01 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01 blanchet 2014-08-01 rationalized preplaying by eliminating (now superfluous) laziness
2014-08-01 blanchet 2014-08-01 removed proof methods as provers from docs
2014-08-01 blanchet 2014-08-01 simplified minimization logic
2014-08-01 blanchet 2014-08-01 tuning
2014-08-01 blanchet 2014-08-01 remove lambda-lifting related assumptions from generated Isar proofs
2014-08-01 blanchet 2014-08-01 whitespace tuning
2014-08-01 blanchet 2014-08-01 remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
2014-08-01 blanchet 2014-08-01 generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
2014-07-31 traytel 2014-07-31 simplified tactics slightly
2014-07-31 blanchet 2014-07-31 cascading timeout in parallel evaluation, to rapidly find optimum
2014-07-30 blanchet 2014-07-30 put faster proof methods first
2014-07-30 blanchet 2014-07-30 use parallel preplay machinery also for one-line proofs
2014-07-30 blanchet 2014-07-30 updated docs
2014-07-30 blanchet 2014-07-30 always minimize Sledgehammer results by default
2014-07-30 blanchet 2014-07-30 tuned ML function name
2014-07-30 blanchet 2014-07-30 reduced preplay timeout to 1 s
2014-07-30 blanchet 2014-07-30 added more proof methods for one-liners
2014-07-30 blanchet 2014-07-30 unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
2014-07-30 fleury 2014-07-30 Improving robustness and indentation corrections.
2014-07-30 fleury 2014-07-30 Skolemization for tmp_ite_elim rule in the SMT solver veriT.
2014-07-30 fleury 2014-07-30 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.