more monotonicity tuning

tuning

added frame component to Gamma in monotonicity calculus

use boolean pair to encode annotation, which may now take four values

started generalizing monotonicity code to accommodate new calculus

merged

handle "max_relevant" uniformly

honor the default max relevant facts setting from the SMT solvers in Sledgehammer

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?

return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction

trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases

reraise interrupt exceptions

[mq]: sledge_binary_minimizer

correcting usage documentation in mirabelle tool

adding mutabelle as a component and an isabelle tool to be used in regression testing

commenting out sledgehammer_mtd in Mutabelle

removing declaration in quickcheck to really enable exhaustive testing

adding timeout to try invocation in mutabelle

adding filtering, sytactic welltyping, and sledgehammer method in mutabelle

replace `type_mapper` by the more adequate `type_lifting`

moved bootstrap of type_lifting to Fun

replace `type_mapper` by the more adequate `type_lifting`

avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;

IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;