2010-12-06 blanchet proper handling of assignment disjunctions vs. conjunctions
2010-12-06 blanchet adapt monotonicity code to four annotation types
2010-12-06 blanchet more monotonicity tuning
2010-12-06 blanchet tuning
2010-12-06 blanchet added frame component to Gamma in monotonicity calculus
2010-12-06 blanchet use boolean pair to encode annotation, which may now take four values
2010-12-06 blanchet started generalizing monotonicity code to accommodate new calculus
2010-12-06 blanchet merged
2010-12-06 blanchet handle "max_relevant" uniformly
2010-12-06 blanchet honor the default max relevant facts setting from the SMT solvers in Sledgehammer
2010-12-06 blanchet have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
2010-12-06 blanchet return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
2010-12-06 blanchet trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
2010-12-06 blanchet reraise interrupt exceptions
2010-12-06 blanchet [mq]: sledge_binary_minimizer
2010-12-06 bulwahn correcting usage documentation in mirabelle tool
2010-12-06 bulwahn adding mutabelle as a component and an isabelle tool to be used in regression testing
2010-12-06 bulwahn commenting out sledgehammer_mtd in Mutabelle
2010-12-06 bulwahn removing declaration in quickcheck to really enable exhaustive testing
2010-12-06 bulwahn adding timeout to try invocation in mutabelle
2010-12-06 bulwahn adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
2010-12-06 haftmann replace `type_mapper` by the more adequate `type_lifting`
2010-12-06 haftmann moved bootstrap of type_lifting to Fun
2010-12-06 haftmann replace `type_mapper` by the more adequate `type_lifting`
2010-12-06 wenzelm avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
2010-12-05 wenzelm IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
2010-12-05 wenzelm command 'notepad' replaces former 'example_proof';
2010-12-05 wenzelm prefer 'notepad' over 'example_proof';
2010-12-05 haftmann merged
2010-12-04 haftmann more intimate definition of fold_list / fold_once in terms of fold
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip