define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;

NEWS for 31afce809794;

reverted cb17feba74e0, avoid sweeping garbage under the carped (MaSh should not create .pyc files anymore, see also 778b2b8f4a35, 347f743e8336);

semicolon is minor keyword (see also 29f1e53f9937);

tuned proof;

more user aliases;

propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;

simplified inner syntax;

added lemma

Merge

Restored Suc rather than +1, and using Library/Binimial

killed 'More_BNFs' by moving its various bits where they (now) belong

hide 'csum' etc.

installed by Johannes in Extended now

merged

hide Fin in output of value via postprocessor; no hinding needed elsewhere

hide extended.Fin in code generator output

no document for Cartouche_Examples: avoid problems typesetting "\001";

NEWS;

merged

tuned;

observe local syntax mode (according to e3a39dae2004, which was lost in 0f3ad56548bc), e.g. relevant for "abbreviation (output)" with non-terminating syntax;

clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;

Locales paper has appeared in print.

tuned spelling;

removed junk;

merged

tuned;