proper transfer rule format for map_transfer

merged

eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates

removed obsolete HOL-Boogie session; keep examples that also test SMT solvers, using a minimal version of the old Boogie loader

transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)

separate ML interface to note facts of a bnf

transfer rule for map (not yet registered as a transfer rule)

tuned exercises

clarified option name, with improved sort order wrt. "time" options;

document update at high priority -- important;

option editor_execution_priority;

obscure options;

print_state at high priority -- fast and important;

proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);

old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);

just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);

turned pattern unify flag into configuration option (global only);

merged

permissive uncheck -- allow printing of malformed terms (e.g. in error messages);

added exerciese

do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)

modify background theory where it is actually required (cf. 51dfdcd88e84);

tuned messages -- avoid text folds stemming from Pretty.chunks;

proper system options for 'find_theorems';

guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;

provide global operations as well;

tuned signature;

tuned;