clarified parser;

tuned signature;

proper positions for inlined command messages, e.g. for completion within theory header;

tuned signature;

clarified modules;

tuned signature;

clarified checks (see f34f5c057c9e);

clarified signature;

tuned comments;

tuned;

typo

more on signed division

clarified files;

tuned whitespace;

clarified parsing vs. semantic errors;

clarified signature;

added document antiquotation @{tool}; formal check of isabelle tools via Isabelle/Scala;

more robust isabelle_scala_files; clarified evaluation;

avoid conflicting base names;

clarified protocol: Doc.check at run-time via Scala function;

more antiquotations (reverting 4df341249348);

tuned;

tuned signature --- more explicit types;

more positions;

support for Scala compile-time positions;

clarified modules;

more robust (amending a4d7da18ac5c);

merged

merged

More removal of apply

merged

more flexible syntax for theory load commands via Isabelle/Scala;

clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically; propagate blob src_path from Scala to ML; clarified signature;

proper structural equality;

more explicit types;

unused (see 7634d33c1a79);

clarified signature;

clarified modules;

clarified file names;

tuned signature;

refined syntax for bundle mixins for locale and class specifications

store timings for used_theories in canonical order, with reconstructed store.read_theories;

merged

merged

Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy

merged

tuned

removed assumptions in lemma (Stepan Holub)

merged

more exports from rendering; suppress empty exports;

clarified signature;

clarified options: batch-build has pide_reports disabled by default (requires significant resources);

tuned;

proper return code for more errors (amending d892f6d66402);

more exports, as in "isabelle dump";

tuned;

clarified signature;

clarified signature: initial markup is_empty, not init_markup;

clarified signature: prefer high-level Snapshot over low-level Command.State;

tuned;

more strict;

clarified signature;

tuned;

clarified signature;

clarified signature --- avoid repeated open_database on server;

renaming

merged

recovered document output from 6bc199a70bf9;

clarified command_timings protocol;

more robust: include reports from Thy_Output.present_thy/output_document;

more complete report positions, notably for command 'back' (amending eca176f773e0);

tuned signature;

clarified signature;

unused;

unused;

tuned;

removed pointless case: messages should always carry proper position;

clarified names;

eliminated pointless transaction;

tuned signature;

clarified document_output vs. progress;

clarified: more uniform;

more robust;

clarified signature and database layout;

clarified messages;

unused (see ac7ae5067783, 1c451e5c145f);

unused;

support for PIDE markup in batch build (inactive due to pide_reports=false);

clarified signature;

proper output of document sources (cf. d892f6d66402);

proper parsing of TSTP HOL lines

proper defn of a heap

merged

cleanup of old proofs

proper output directory (amending cc1347c8c804);

updated to cvc4-1.8;

clarified signature: prefer Database_Context;

clarified modules;

tuned NEWS;

removed unused material;

more NEWS;

NEWS;

more interrupts;

clarified messages;

clarified document output;

clarified messages;

clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);

tuned signature;

more standard imports;

tuned signature;

generate theory HTML in Isabelle/Scala; discontinued HTML support in Isabelle/ML;

merged

Add support for CVC4 1.8 to Sledgehammer

proper meta_digest: avoid non-portable position information;

clarified messages;

proper message;

clarified signature;

clarified modules;

more robust library_call (again): dynamic file name, static symbol;

updated to polyml-test-7e49fce62e3d --- follow current ongoing development;