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;

prefer rail cartouche -- avoid back-slashed quotes; proper documentation of \<newline> syntax;

tuned signature;

avoid breakdown of document preparation, which does not understand cartouche tokens yet;

more cartouche examples, including uniform nesting of sub-languages;

inner syntax token language allows regular quoted strings; tuned signature;

tuned signature;

tuned error messages, more accurate position;

tuned -- more direct err_prefix;

clarified scan_cartouche_depth, according to Scala version; more accurate error position;

tuned errors;

whitespace tuning

whitespace tuning

made SML/NJ happier

made SML/NJ happier

updated NEWS

merged

removed theory dependency of BNF_LFP on Datatype

made SML/NJ happier

removed dependency on 'Datatype' structure

made SML/NJ happier

compile

compile

technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'

swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)

moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'

renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)

hide BNF notation

moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

rationalized lemmas

move BNF_LFP up the dependency chain

compile

updated docs

have Nitpick lookup codatatypes

removed dependency of BNF package on Nitpick

deactivate one more cardinal notation

fixed typo

compile

dissolved BNF session

rationalized dependencies

reduced dependencies + updated docs

minimized Nitpick's dependencies

moved BNF examples

rationalized dependencies

moved hide_const from BNF to Main

updated README

tuned names

tuning

compile

killed obsolete session

tuned comment

made BNF compile after move to HOL

adjusted comments

avoid nested 'Tools' directories

tuned comments

moved BNF files to 'HOL'

kill notations

renamed '_FP' files to 'BNF_' files

tuning

moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'

tuned names

spelling

killed obsolete provers from documentation

merged

removed obsolete remote_cvc3 and remote_z3

implicit "cartouche" method (experimental, undocumented);

more examples;

cartouche within antiquotation;

cartouche within nested args (attributes, methods, etc.);

group symbols;

prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers