tuned proofs -- less legacy;

tuned message;

tuned proofs;

renamed method "goals" to "goal_cases" to emphasize its meaning;

tuned proofs;

method "goals" ignores facts;

tuned;

unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification; also unconceal corresponding primitive definitions, which are official conversions between predicates and sets

fully detached test run, to avoid flashing window on Windows with Cygwin-Terminal;

single-instance application on Windows;

more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;

convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;

clarified order;

more symbols;

Unicode is standard in Poly/ML repository version;

removed obsolete undocumented feature;

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;