more standard local_theory operations; eliminated slightly odd @{cpat};

HOL-Proofs is slow;

convenient access to application properties;

tuned -- avoid slightly odd @{cpat};

dropped redundant NEWS

less ambitious options, to accomodate 4GB systems;

tuned

clarified declaration flags, like 'declaration' command;

merged

simplified simproc programming interfaces;

eliminated \<Colon> from syntax of constraints;

eliminated \<Colon> -- from dead code!

merged

reactivate examples with predicate compiler and quickcheck

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;

proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";

merged

merged

use quotient and lifting package; drop dysfunctional setup for the code generator

merged

new lemmas about vector_derivative, complex numbers, paths, etc.

trim context for persistent storage;

misc tuning and modernization;

use open/close_target rather than Local_Theory.restore to get polymorphic definitions;

clean name as in ML Completion.make;

use alphabetic order before history order;

eliminated pointless cterms;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage; clarified thm equality;