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;

proper option, not catch-all pattern;

support x86_64-windows;

prefer symbols;

prefer symbols;

proper qualified naming;

misc tuning and clarification;

misc tuning and modernization;

clarified context;

tuned signature;

clarified context;

tuned message;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage;

trim context for persistent storage;

store result of swapify, to avoid later access to implicit context;

trim context for persistent storage;

tuned;

clarified implicit context;

clarified exceptions; tuned signature;

clarified exceptions; more careful treatment of missing context;

trim context for persistent storage;

trim context for persistent storage;

clarified exceptions;

tuned documentation -- merge is implicitly performed by the system;

clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);

more abstract theory certificate, which is not necessarily the full theory;

eliminated obsolete environment variable

tuned signature;

tuned;

tuned;

tuned signature;

tuned;

tuned signature;

clarified language context, e.g. relevant for symbols;

merged;

tuned;

generate proper error instead of exception if goal cannot be atomized

standardized some occurences of ancient "split" alias

more lemmas on sorting and multisets (due to Thomas Sewell)

robust handling of Vampire 4 proofs

reverted 6ac3172985d4 -- the old URL has been restored

fixed typo in comment

use fancy options of Java 8;

tuned signature;

clarified kill on Windows: just one executable;

avoid deprecated PluginOptions with its unbounded window size;

clarified undefined_blobs: already loaded theories are suppressed; enabled jedit_auto_resolve (again): e.g. relevant for debugging when following links through source files;

tuned spacing

tuned exercise

merged

reset focus after thread update (with new debug_states);

atomic Debugger.status; output without thread context is empty; tuned;

tuned;

tuned;

more thorough GUI update;

maintain per-thread focus context; tuned signature;

typos

nex exercise

more explicit debugger caret rendering;

more explicit type Debugger.Context;

more precise tree re-selection;

proper GUI event;

update focus more thoroughly;

tuned;

merged

don't use types that come from the database---they are inconsistent with the ones occurring in the terms

tuned;

clarified linux application bundle;

more version information;

separate bundle for windows64;

tuned;

more scalable GUI;

eliminated WinRun4J artifact; tuned;

proper classpath for launcher; proper use of jdk/x86-windows; misc tuning;

updated to jdk-8u60, with support for x86_64-windows;

updated to recent launch4j 3.8;

clarified modules;

clarified modules, like ML version;

clarified modules, like ML version;

suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;

obsolete;

tuned signature, according to ML version;

The Stone-Weierstrass theorem

tuned;

obsolete;

NEWS;

updated to polyml-5.5.3-20150820, with native x86-windows support;

precise BinIO, without newline conversion on Windows;

repaired proofs after 6a6f15d8fbc4;

merged

clarified x86-windows setup;

proper check for Windows executables;

Cygwin bash on Windows;

tuned;

avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;

New material and fixes related to the forthcoming Stone-Weierstrass development

disabled auto resolve, until practical consequences are more clear;

example options;

proper platform_path;

clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations); avoid patching of SML basis library;

SOMEthing went wrong in eb87fc42825c;

include libgmp;

proper platform path for intial PolyML.SaveState.loadState; tuned signature;

proper platform path for initial load;

tuned signature;

keep native CInterface to make SHA1 work properly;

more setup for native Windows (Pure and HOL session with image);

basic setup for native Windows (RAW session without image);

more complete build;

support for native x86-windows via MinGW32;

no ML_debugger support in Pure -- too complicated;

more careful propagation of ML_debugger option to Pure;

support for ML files with/without debugger information;

explicit debug flag for ML compiler;

tuned;

abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);

clarified initial ML name space (amending 7aad4be8a48e);

produce certified vars without access to theory_of_thm, and without context;

produce certified vars without access to theory_of_thm, and without context;

tuned;

added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);

prefer theory_id operations; tuned signature;

separate type theory_id;

delete precisely the added rules; tuned;

clarified context;

tuned whitespace;

tuned signature;

tuned;

tuned whitespace;

tuned whitespace;

obsolete;

clarified context;

clarified context;

tuned GUI;

proper setup of evaluation context;

tuned;

more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;

allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);

tuned signature;

qualified adjust_*