clarified settings -- avoid hard-wired directories;
tuned documentation;

full benchmarks, including all conditional theories;

clarified store directories;
discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;

more Java heap, e.g. relevant for hg.graph on Isabelle repository;

more accessible src/Pure/ROOT.ML;

more explicit latex errors;

updated to jdk-8u152, which is for x86_64 only;

more uniform isabelle_scala;
more uniform ISABELLE_SCALAC_OPTIONS with heap options;

updated to jvm-1.8;

clarified settings;

discontinued global etc/abbrevs;

gnuplot presentation similar to former isatest-statistics;

prefer HTTPS;

renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;

back to external line editor, due to problems of JLine with multithreading of in vs. out;

isabelle console is based on Isabelle/Scala;

SML/NJ is no longer supported;

back to elementary options used in Isabelle2015 for jdk-7 -- none of the intermediate experiments for jdk-8 improved reactivity on particular dual-CPU system, but the problem seems to be absent on common single-CPU systems;

eliminated somewhat pointless and obscure options;

tuned java options;

support additional abbrevs;

some GC options that potentially improve reactivity;

Isabelle fonts via external component;

back to old-fashioned GC, which appears to work better with interactive applications;

less ambitious options, to accomodate 4GB systems;

clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);

clarified ISABELLE_BUILD_JAVA_OPTIONS;

use fancy options of Java 8;

more uniform headless mode for all derivatives of "build" (amending df5dc24ca712);

added Par_List in Scala, in accordance to ML version;
system property "isabelle.threads" determines size of Scala thread pool, like system option "threads" for ML;
avoid ".par" framework with its hard-wired thread pool, which also has problems with cancellation;
tuned;

more paranoia settings, e.g. relevant for Ubuntu 15.04;

prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;

more release notes;

tuned comments;

"isabelle tty" is superseded by "isabelle console";

--HG--
rename : lib/Tools/tty => lib/Tools/console

tuned options for scalac;

updated to scala-2.11.0 with classpath provided by its etc/settings;

no need to copy jars, after regular use of classpath in 793a429c63e7;

proper settings instead of hard-wired information;

misc tuning and clarification;

tuned comments;

generic $ISABELLE_OPEN;

clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;

prefer "fresh" open -- requires Lion / Mountain Lion;

unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;

clarified directory structure;

maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
ignore $ISABELLE_JAVA_EXT -- do not change java.ext.dirs;

provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;

tuned comments;

discontinued historic document formats;

discontinued ISABELLE_DOC_FORMAT;

discontinued obsolete "isabelle print";

prefer Safari for viewing PDF files, which appears to be better behaved than Preview concerning re-opening recent files (Mountain Lion);

discontinued obsolete isabelle usedir, mkdir, make;

more generous java resources via ISABELLE_BUILD_JAVA_OPTIONS;

decentralized historic settings;

accomodate encrypted file-system on linux;

eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;

provide polyml-5.4.1 as regular component;
discontinued old-style choosefrom settings with hardwired defaults;

added "isabelle components" tool;

discontinued special treatment of Proof General;

proper shell variable;

further imitation of ISABELLE_USEDIR_OPTIONS via options;

tuned;

updated smlnj settings;

discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);

slightly modernized ISABELLE_GHC etc. -- /usr/bin is more likely to provide it by default (notably on macbroy2[0-9] and lxbroy*);

smarter PDF_VIEWER defaults, based on hints by Lars Noschinski;

prefer evince over old xpdf -- NB: x86-cygwin bundles its own application;

USER_HOME settings variable points to cross-platform user home directory;

removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare

clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
clarified jEdit/README_BUILD;

updated comments;

ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
update for prospective jdk1.7.x component;

less noisy Isabelle/Scala build process;

more robust ISABELLE_HOME_USER for repository versions -- some versions of Emacs interpret foo//bar as /bar even on the command-line (unlike regular POSIX semantics);

updated to polyml-5.4.1;

discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;

specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;

provide Isabelle/Scala environment as Java extension, instead of user classpath
(which is subject to adhoc changes);

clarified default ML settings;

simplified/generalized ISABELLE_FONTS handling;

example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;

files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;

some cleanup of old-style settings;

clarified ISABELLE_CSDP setting (formerly CSDP_EXE);

Apple's way of locating java;

updated for polyml-5.4.0;
discontinued old-fashioned POLY_HOME via path;
more robust handling of polyml-version, preferably provided by Poly/ML distribution itself;

more robust determination of java executable;

more robust treatment of spaces in file names;

moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;

assume given SCALA_HOME, e.g. from component settings or external setup;

use proper ISABELLE_PLATFORM instead of adhoc uname;

rendering information and style sheets via settings;
generalized Isabelle_System.try_read;
prefer getenv_strict in most situations;

refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;

polyml-platform script is superseded by ISABELLE_PLATFORM;

improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;

removed ever experimental support for Moscow ML -- hardly works anymore;

discontinued special HOL_USEDIR_OPTIONS;

deactivated default for E_HOME, SPASS_HOME -- now configured as components;
deactivated default for VAMPIRE_HOME -- superceded by remote_vampire;

setup for official Poly/ML 5.3.0, which is now the default;

--HG--
rename : src/Pure/ML-Systems/polyml.ML => src/Pure/ML-Systems/polyml-5.2.ML
rename : src/Pure/ML-Systems/polyml-experimental.ML => src/Pure/ML-Systems/polyml.ML

tuned ML_OPTIONS for SML/NJ -- for improved performance;

PDF_VIEWER: more Unix-ish behaviour on Mac OS;

removed jedit setup -- now a self-contained component (external);

misc changes to SOS by Philipp Meyer:
CSDP_EXE as central setting;
separate component src/HOL/Library/Sum_Of_Squares;
misc tuning and rearrangement of neos_csdp_client;
more robust treatment of shell paths;
debugging depends on local flag;
removed unused parts;

--HG--
rename : lib/scripts/neos/NeosCSDPClient.py => src/HOL/Library/Sum_Of_Squares/neos_csdp_client
rename : src/HOL/Library/sos_wrapper.ML => src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
rename : src/HOL/Library/sum_of_squares.ML => src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML

basic support for components (which imitate the usual Isabelle directory layout);

ISABELLE_USEDIR_OPTIONS: -q 2 by default;

parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;

SCALA_HOME: proper line escapes for choosefrom;

observe SCALA_HOME, if available;
no default classpath for scala-library.jar;

back to default -M max, with more robust interpretation of corresponding max_threads value;

example settings for Poly/ML 5.3 (experimental);

retrieve ML source files;

uniform default settings for E, Vampire, SPASS;

updated example settings;

discontinued support for Poly/ML 4.x versions;

ISABELLE_USEDIR_OPTIONS: less ambitious -M1 by default -- multithreading is largely untested on fringe platforms (cygwin, solaris);

suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;

Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.

Merge.

discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;

Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it).
These changes have no inpacts on already working Isabelle installations.

removed vampire-wrapper (remote-script covers that)

more sophisticated MacOS interface script (mostly for Carbon Emacs);
no longer include MacPorts path;
simplified default PROOFGENERAL_OPTIONS, removed PROOFGENERAL_EMACS;

removed Ids;

ISABELLE_USEDIR_OPTIONS: -M max is default;

uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;

removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;

default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;

less ambitious default for JEDIT_JAVA_OPTIONS;

JEDIT_OPTIONS: moved -settings to interface script (more robust);

make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;

added jEdit settings;

simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;

Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);

added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;

added PROOFGENERAL_HOME;

add scala-library.jar if available;

added ISABELLE_SCALA, ISABELLE_JAVA;

added JVM components (Scala or Java);

removed experimental Poplog/PML support;

removed obsolete thumbpdf;

removed obsolete THIS_IS_ISABELLE_BUILD feature;
moved external provers further up;
no HOL4_PROOFS by default;

ISABELLE_LINE_EDITOR: prefer rlwrap, which passes interrupts properly;

* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;

added ISABELLE_LINE_EDITOR;
tuned;

polyml: default heap size is back to -H 200 (people are still using
machines with < 1GB of memory; no need to workaround heap problems of
polyml-5.0 anymore);

tuned comments;

tuned;

platform-sensitive default location for ATP provers

Auto-config of E_HOME, SPASS_HOME, VAMPIRE_HOME

renamed POLYML_LINK_OPTIONS to POLY_LINK_OPTIONS;

added POLYML_LINK_OPTIONS, which is required for unusual platforms (notably cygwin);

HOL_USEDIR_OPTIONS: no special -M setting (now works with multithreaded);

HOL_USEDIR_OPTIONS: default to -M 1 (more robust);

added jEdit mode spec;
tuned comments;

increase default max heap size for poly to -H 500 (this is what isatest uses,
-H 80 is not enough for HOL on at-mac-poly).

added ISABELLE_FILE_IDENT (command line for source file identification);

tuned USEDIR_OPTIONS;
PDF_VIEWER: try to be smart for MacOS (Darwin);

tuned comments

tuned comments;

setup for polyml-5.0;

ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;

HOL_USEDIR_OPTIONS: -p 1 by default;

increased heap size for polyml-4.9.1;

added Poly/ML 4.9.1 (experimental!);

added support for MiniSat 1.14

fixed example;

simplified polyml example;

added simplified settings for Poly/ML 4.x (commented out);

reverted (accidental?) change of 1.148;

Merged theory ResAtpOracle.thy into ResAtpMethods.thy

moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!

Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").

tuned;

Poplog/PML: ML_SUFFIX=.psv;

added Poplog/PML version 15.6/2.1 (experimental!);

PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);

pointers to src/HOL/Tools/sat_solver.ML added in comments

no longer prefer xemacs, which fails more often than GNU emacs;

tuned;

-V outline=/proof,/ML;

tuned ML_OPTIONS;

tuned;

polyml: use polyml-platform/version from Isabelle distribution;
removed DEFS_CHAIN_HISTORY;

1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML

retract accidental user commit;
removed obsolete XSYMBOL_HOME;
tuned;

proving bounds for real linear programs

added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy

updated;

#SMLNJ_CYGWIN_RUNTIME=1

renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
tuned;

removed ISAMODE settings;

added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)

added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)

removed --version which is not a valid polyml flag and has no effect

reverted accidental commit of user modification;

Fix automatic determination of poly version.

Removed remaining references to Main.thy in reconstruction code.

Include automatic determination of poly version.

*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT;

*** empty log message ***

Removed practically all references to Library.foldr.

fixed mac line

added ZCHAFF_VERSION

*** empty log message ***

DOCTYPE declaration added

PDF_VIEWER suggestion

display pdf as well as dvi

Merged in license change from Isabelle2004

Jerusat settings added

entries for ZChaff and BerkMin added/modified

added PRINT_COMMAND setting

removed mlworks and smlnj-0.93 (obsolete);

do not mention poly 3.x any more (it is untested)

look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
if no multi platform installation found.

ZCHAFF_HOME variable added

include more explanation of variables

run makeindex if necessary

fixed

set isatool usedir to verbose by default

set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
switched off by default

more documentation

tuned;

wild guess at polyml-4.1.2;

ML_OPTIONS="-h 15000" (used to be 30000);

removed TEXINPUTS;

tuned;

removed installfonts, xterm interface;
improved default of PROOFGENERAL_OPTIONS;

tuned;

ISABELLE_EPSTOPDF="epstopdf";

updated;

ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);

tuned;

tuned;

tuned;

even smarter setup for several installations of Poly/ML 3.x and 4.0;

tuned auto paths;

XSYMBOL_INSTALLFONTS is back;

tentative fix while hunting gremlins ...;

#XSYMBOL_INSTALLFONTS;

added /usr/share/emacs/ProofGeneral/isar/interface choice;

easy settings: add /usr/local prefix;
tuned;

GPLed;

more robust handling of spaces in args / file names;
tuned;

more polyml choices;
tuned;

tuned;

use polyml-version;

choosefrom: easy settings;

X-Symbol mode -- look in canonical place;

Moscow ML 2.00 or later (experimental!);
tuned;

tuned comments;
even smarter guessing of ProofGeneral location;

added site settings check;

Proof General -- if present make this the default;

new Poly/ML setup made default;

fixed comment;

thumbpdf (disabled by default);

added ISABELLE_BIBTEX;

removed TeX environment hacking;

Document preparation setup;

ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);

Mucke, Einhoven;

tuned;

External reasoning tools;

no longer gives a default value to SVC_MACHINE

new variables for SVC

ML_HOME=$ISABELLE_HOME/../smlnj/bin;

$ML_HOME/.arch-n-opsys 2>/dev/null;

smlnj-110 setup made default;

/usr/share/smlnj/bin;

ML_PLATFORM;

improved comment;
removed ISABELLE_INTERFACE_OPTIONS;
added ProofGeneral;

ML_SYSTEM=polyml-3.1;

ML_SYSTEM factory default;

dropped support for SML/NJ 109.x;

MLWorks 2.0;

ISABELLE_USEDIR_OPTIONS="-i false";

replaced $LOGNAME by $USER;

polyml-3.1;

smlnj-110 factory default;

ISABELLE_TMP_PREFIX: $LOGNAME

added mlworks;

polyml-3.1;

make smlnj-110 default;

smlnj-110;

ISABELLE_TMP_PREFIX;

Added Cambridge font server

Added new environment variable ISABELLE_BROWSER_INFO.

removed smlnj-1.07;

polyml-3.1 default again (for local work);

NJ 1.09.2x as factory default!

tuned comment;

remove cl.cam font server;

tuned Isamode stuff;

removed Cambridge font server;

renamed DEFAULT_LOGIC to ISABELLE_LOGIC;

ML_SYSTEM is polyml-3.1 again;

tuned comments;
NJ 1.09.27 now default;

improved comments;

fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);

improved DVI_VIEWER default;

improved fontserver example;

fixed ISAMODE_HOME;

eliminated PLATFORM;

replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;

tuned comments;

added THIS_IS_ISABELLE_BUILD discrimination;

pass xterm mode by default;

tuned comments;

tuned;
removed ISABELLE_SYMBOLS;

added ISABELLE_INSTALLFONTS;

added dvi viewer alternative;

changed xterm geometry;

added ISABELLE_HTML;
fixed Poly/ML 2.x;

major cleanup;
added comments;

added smlnj-0.93;

added DVI_VIEWER for 600dpi fonts;

added ISABELLE_DOCS;

added ISAMODE_HOME;

settings: Isabelle settings -- site defaults.