tuned syntax -- separate tokens;

eliminated pointless check -- command definitions are subject to theory context;

merged

prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;

tuned markup;

tuned;

clarified keyword categories; tuned;

tuned signature;

tuned;

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

proper import for command 'permanent_interpretation';

proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;

more accurate keywords;

tuned signature;

more explicit Keyword.keywords;

proper Keyword.keywords (cf. 82a71046dce8);

prefer explicit Keyword.keywords (cf. 82a71046dce8);

tuned signature;

prefer explicit Keyword.keywords;

simplified keyword kinds; more explicit bootstrap syntax;

Tidying up. Removing unnecessary conditions from some theorems.

more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories

document '*_transfer' attribute

document 'size_neq'

generate 'size_neq' for datatypes

fix 'unfla' function

proper oriented equivalence of dvd predicate and mod

merged

more symbols;

tuned signature;

more uniform header_keywords in ML/Scala; tuned signature;

tuned;