tuned error message;

retrieve imports from document state, with fall-back on theory loader for preloaded theories; misc tuning;

explicit check of finished evaluation;

refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;

simplified exec: eliminated unused status flag;

consistently use variable name 'F' for filters

generalize lemmas about LIM and LIMSEQ to tendsto

HOL-Nominal-Examples: respect distinction between sets and functions

less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;

merged

HOL-Hahn_Banach: use Set_Algebras library

ex/Quickcheck_Examples.thy: respect distinction between sets and functions

clarified Toplevel.end_theory;

simplified Toplevel.init_theory: discontinued special name argument;

simplified Toplevel.init_theory: discontinued special master argument;

provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;

reduced verbosity;

tuned signature;

clarified node header -- exclude master_dir;

tuned;

maintain node header; misc tuning and clarification;

removed unused lemma; removed old-style ;

point isatest-statistics to the right afp log files

IMP/Util distinguishes between sets and functions again; imported only where used.

remove redundant lemma setsum_norm in favor of norm_setsum; remove finiteness assumption from setsum_norm_le;

merged

make more HOL theories work with separate set type

immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029); more careful treatment of last_round on startup/shutdown;

merged

merged