clarified modules;

tuned;

more uniform output: formal comments within {* ... *};

tuned;

clarified output: avoid extra space;

output token content with formal comments and antiquotations;

tuned;

clarified signature;

clarified modules;

inner syntax comments may be written as "\<comment> \<open>text\<close>";

spelling

corrected op

tuned op

tuned op

tuned op

tuned op

tuned op's

tuned op

tuned op

tuned op's

Renamed (^) to [^] in preparation of the move from "op X" to (X)

tuned op

HOL-Analysis: add set_integrable_restrict_space

more correct parentheses

more tight HTML output: avoid extra lines within <pre>;

HTML output for Markdown elements; clarified HTML operations;

updated NEWS

removed dead code

removed old 'add_datatype' ML functions

kill old size infrastructure

repaired whitespace accident from 2505cabfc515

proper namespace for evaluators

tuned

more correct name resolving

skip abstract constructors silently in datatype clauses of computations

removed para about 'old_datatype' in docs

old_datatype no longer exists (cf. 706b1cf7b76d);

merged

PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);

clarified terminology of "markdown_bullet";

compile

updated dependencies + compile

moved 'realizers' into their own theory, now that they are decupled from the old datatype construction

removed 'old_datatype' command

don't test 'old_datatype', which is on its way out

ported inductive realizer to new datatype package

removed needless theorems

store high-level 'size' equations

avoid call to function that may throw an exception in error message

misc tuning and modernization;

more completion templates;

proper purge of auxiliary bibtex theory;

tuned signature;

tuned;

Restored correct spacing for set comprehensions

less redundant;

more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);

more robust treatment of conflicts with existing Unicode text;

tuned whitespace;

no check for bibtex entries from other sessions;

clarified signature;

more accurate message patterns;

prefer formal citations; more accurate bibtex entries;

proper bibtex entries;

formal check of @{cite} bibtex entries -- only in batch-mode session builds;

clarified check, notably for bibtex theory (amending 5f082b1fa9fa);

NEWS;

proper check for imports, not just ROOT entries;

tuned signature;

implicit thy_load context for bibtex files (VSCode);

bibtex theory is always required and thus eventually consolidated;

implicit thy_load context for bibtex files;

clarified signature: prefer Document.Node.Name.is_bibtex;

avoid spurious noise: Prover IDE is meant to check for errors;

clarified signature;

avoid clash with special files in HTML output;

unused;

tuned signature;

prefer existing Resources.check_path;

more accurate bibtex entries;

added command 'bibtex_file' (for PIDE interaction only);

clarified default position for empty message pos;

spelling

Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume

fewer warnings;

clarified positions;

check bibtex database on ML side -- for semantic PIDE editing; tuned signature;

clarified directories;

more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);

check bibtex database: errors and warnings;

more symbols;

Merge

Merge

new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

more symbols;

tuned;