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;

command 'notepad' replaces former 'example_proof';

prefer 'notepad' over 'example_proof';

merged

more intimate definition of fold_list / fold_once in terms of fold

canonical fold signature

formal notepad without any result;

added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;

eliminated obsolete Token.Malformed -- subsumed by Token.Error;

tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);

added Syntax.pretty_priority;

merged

conventional point-free characterization of rsp_fold

replaced memb by existing List.member

explicit type constraint; streamlined notation

tuned proposition

lemma multiset_of_rev

lemmas fold_remove1_split and fold_multiset_equiv