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;