tuned;

standardized aliases;

transfer rule for {c,d}tor_{,un}fold

two useful relation theorems

factored syntactic type classes for bot and top (by Alessandro Coglio)

derive specialized version of full fixpoint induction (with admissibility)

export mono_thm

merged Def_Init_Sound_X into Def_Init_X

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