tuned signature;

Merge

Massive revisions, as a valid path must now be continously differentiable (C!)

isabelle update_cartouches; tuned proofs; tuned whitespace;

isabelle update_cartouches;

recode all text, which is relevant for Session.save on non-ASCII directory;

tuned;

more recent JavaAppLauncher, which supports file associations;

more explicit indication of bundled jdk, which is required for newer versions of JavaAppLauncher;

more app properties glimpsed from infinitekind/Moneydance 2015.5;

tuned whitespace;

updated to polyml-5.5.3-20150916 (polyml git version cb1b36caa242);

avoid module dependency cycles

goali -> i

Omega_Words_Fun: Infinite words as functions from nat.

provide FontMapper for embedded fonts;

avoid hardwired colors; more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);

avoid hardwired colors;

replacement character for spaces;

single-instance application, even on Linux;

single-instance application for Linux;

tuned message;

added isabelle jedit_client;

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;

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;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage;

more thorough transfer;

clarified context;

more thorough transfer;

clarified context;

tuned message;

trim context for persistent storage;

trim context for persistent storage;

eliminated old 'defs';

expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;

clarified vacuous binding;

trim context more thoroughly;

tuned;

updated sessions;

thread context for exceptions from forks, e.g. relevant when printing errors; tuned signature;

eliminated \<Colon>;

tuned -- avoid slightly odd @{cpat};

support x86_64-windows;

misc tuning and simplification;