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;