added choice operator output for Satallax

rationalized option names -- mono becomes raw_mono and mangled becomes mono

handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards

avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics

fixed bang encoding detection of which types to encode

lemma Compl_insert: "- insert x A = (-A) - {x}"

avoid variable clashes by properly incrementing indices

improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

include chained facts for minimizer, otherwise it won't work

remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway

back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;

tuned Session.edit_node: update_perspective based on last_exec_offset;

tuned signature -- iterate subsumes both fold and get_first;

further clarification of Document.updated, based on last_common and after_entry; tuned;

tuned signature;