clarified session sources: theory and blobs are read from database, instead of physical file-system;

tuned;

clarified signature: more operations;

clarified signature: more operations;

tuned;

more direct access to session_sources, without somewhat fragile file-system operations;

tuned;

tuned signature;

tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;

clarified signature: old node is ignored;

tuned;

clarified signature;

final tidying of theorems

merged

merged

continued proof simplification

merged

Further simplifications

More tidying of proofs

tuned;

merged

discontinued fragile operation;

more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;

tuned whitespace;

tuned;

avoid somewhat fragile Document.Node.Name.master_dir_path;

clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;

tuned;

clarified modules;

tuned;

tuned;

clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;

tuned signature: avoid too many aliases (see also 72daee8a39ca);

clarified modules;

merged

strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp

Fixed a couple of simple_path occurrences

merged

Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"

clarified signature: more explicit types;

more robust: prefer internal theory names;

clarified session_sources (again, see also 9d0e6ea7aa68);

clarified signature: more explicit types;

tuned output;

clarified signature: more general operations;

clarified signature: more explicit types;

clarified signature: more explicit types (see also 90c552d28d36);

do write_session_sources early, to have information available in build job;

tuned signature, following Url.append_path;

do not bundle Isabelle/Naproche, while it keeps changing;

tuned signature;

tuned;

clarified signature: uniform master_dir instead of separate field;

more standard master_dir;

tuned signature, following Url.append_path;

merged

more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;

store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions; enforce rebuild of Isabelle/ML to update build databases;

tuned signature;

tuned;