added one more known Z3 failure

added config options to control two aspects of the translation, for evaluation purposes

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;

improved Document.edit: more accurate update_start and no_execs; tuned;

refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;

tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;

maintain last_execs assignment on Scala side; prefer tables over IDs instead of objects;

propagate information about last command with exec state assignment through document model;

tuned signature;

slightly more abstract Command.Perspective;

slightly more abstract Text.Perspective;

tuned proofs;

tuned syntax -- avoid ambiguities;

more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");

delete commented-out dead code

merged