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;