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

make Multivariate_Analysis work with separate set type

make HOLCF work with separate set type

merged

avoid duplicate rule warnings

modify euclidean_space class to include basis set

remove lemma stupid_ext

documented extended version of case_names attribute

normalized theory dependencies wrt. file_store;

general Graph.schedule;

allow "$" within basic path elements (NB: initial "$" refers to path variable);

clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);

simplified class Thy_Header;

clarified Exn.message;

uniform treatment of header edits as document edits;

explicit datatypes for document node edits;