merged

simplified;

obsolete;

isabelle console -r" helps to bootstrap Isabelle/Pure;

discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;

proper return code (cf. faa452d8e265);

clarified isabelle_process;

clarified modules; tuned signature;

clarified modules;

clarified modules;

removed junk;

discontinued polyml-5.3.0;

made Nitpick more robust

constructive formulation of factorization

support for ML_exception_debugger;

respect qualification when noting theorems in prim(co)rec

added invariant proofs to AA trees

tuned signature;

clarified modules;

load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature;

clarified modules;

clarified modules;

ML debugger support in Pure (again, see 3565c9f407ec);

use bootstrap compiler earlier;

merged

merged

removed obsolete chmod: isabelle_process no longer supports writable heaps;

redundant -- already provided by Poly/ML toplevel;

prefer bash_process;

only one nested bash process (NB: OS.System = vfork + exec /bin/sh in RTS is faster than Posix.Process.fork/exec in ML);

generalized ML function

tuned bootstrap order to provide type classes in a more sensible order

missing file;

clarified session; tuned headers;

tuned header;

simplified -- always produce heap for RAW, Pure;

merged

isabelle_process executable no longer supports writable heap images;

more careful cleanup;

obsolete;

tuned;

redundant -- already part of Session.finish;

proper exit as in Scala version (in contrast to a45ba78abcc1);

save heap more directly;

clarified modules;

clarified ML heap operations;

generalized

Merge

Merge

the integral is 0 when otherwise it would be undefined (also for contour integrals)

removed junk;

merged

clarified;

support only polyml-5.3.0 and polyml-5.6;

Merged

Minor adjustments to euclidean rings

proper document source;

simplified / unified isatest settings;

tuned signature;

discontinued old 'header';