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

change some subsection headings to subsubsection

remove unnecessary lemma card_ge1

move connected_real_lemma to the one place it is used

merged

make sure that all facts are passed to ATP from minimizer

more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"