single-letter abbrev does not make sense -- too many candidates;

allow short words for explicit completion;

fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;

more symbol abbrevs;

misc tuning -- reduce conflicts;

allow multiple entries;

more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;

allow multiple symbol properties, notably groups and abbrevs;

private copy (!) of etc/symbols for WWW_Find, which has its own interpretation of the file format;

check tar error, e.g. from corrupted download;

less surprising immediate completion;

updated keywords

tuned theory name

moved keywords down the hierarchy

renamed command to clarify connection with BNF

merged two theory files

updated news/contributors with BNF stuff

added example

rationalized files

polished newly included files after moving

moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository

tuned proofs;

merged

qualify internal and external constants in {l,g}fp properly

merged

merged

border as for Pretty_Tooltip;

less aggressive immediate completion, based on input and text;

preserve original word -- relevant for true uniqueness of immediate completion;

tuned;