report malformed symbols;

qualified Symbol_Pos.symbol;

total Symbol.source;

eliminated slightly odd pervasive Symbol_Pos.symbol;

treat Unicode "replacement character" (i.e. decoding error) is malformed;

simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);

tuned;

back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;

await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

updated README;

defensive defaults for more robust experience for new users;

merged

preliminary support for newer versions of Z3

turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user

let the theory formally depend on the Boogie output

look for certificates relative to the theory

dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT

merged

update Theory.requires with new theory name

tuned signatures;

never open Unsynchronized;

merged

section headings

reorder chapters for generated document

merge Representable.thy into Domain.thy

move stuff from Domain.thy to Domain_Aux.thy

move map functions to new theory file Map_Functions; add theory file Plain_HOLCF

allow unpointed lazy arguments for definitional domain package

add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas

merged