provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;

uniform abbrevs for left/right arrows;

more abbrevs according to Isabelle/HOL ASCII replacement syntax;

added common alternative for == (its ambiguity also avoids conflict with ==>); clarified (= )= [= ]= (like <= >=); removed * (too intrusive);

more accurate description: Swing/L&F has additional handlers;

handle selector formulae with no corecursive calls

merged

tuned proofs;

simplified (see 7c39677f9ea0);

sort items according to persistent history of frequency of use;

more general backup files;

fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)

some tests on /home/polyml/polyml-svn, which is approaching polyml-5.5.1;

tuned proofs;

Doc improvements

prove theorem in the right context (that knows about local variables)

fixed docs w.r.t. availability of "primrec_new" and friends

more canonical naming

more set syntax

merged

NEWS;

more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);

explicit is always immediate;

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;

added action isabelle.complete, using standard jEdit keyboard shortcut;

option to insert unique completion immediately into buffer;

tuned proofs;