disable jedit_auto_resolve (again) -- too confusing;

proper Windows path, notably for ML basis;

more basic Windows path operations -- evade exception InvalidArc with Unicode;

updated to polyml-5.5.3-20150908, with support for x86_64-windows and Unicode file-names;

clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);

clarified Java runtime options for 32 vs. 64 bit;

clarified JEDIT_JAVA_OPTIONS: separate defaults for 32 vs. 64 bit;

clarified JEDIT_JAVA_SYSTEM_OPTIONS;

clarified ISABELLE_BUILD_JAVA_OPTIONS;

unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup

parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; with explicit regression setup

formally regenerated

tuned notation, proofs, namespace

obsolete: if case_prod is fully applied, it is printed as proper case expression; eta-contracted variants are read best as "uncurry" combinator

prefer "uncurry" as canonical name for case distinction on products in combinatorial view

tuned

obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised

dropped whitespace leftover from b57df8eecad6

do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';

tuned proofs;

removed obsolete theory Legacy_Mrec;

NEWS;

merged

close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;

modernized name space management -- more uniform qualification;

tuned -- do not open ML structures;

trim context for persistent storage;

trim context for persistent storage; tuned signature;

proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;

more general Typedef.bindings; tuned signature;