avoid accidental handling of interrupts; interrupts have no properties;

unused;

tuned signature -- clarified modules;

avoid spam in position reports;

tuned signature;

take qualification of type name more seriously: derived consts and facts are qualified uniformly;

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';

more official "isabelle check_sources";

removed pointless "isabelle yxml";

moved getopts to Scala;

moved getopts to Scala;

obsolete;

obsolete;

moved getopts to Scala;

moved getopts to Scala;

tuned;

just one File.find_files, based on Java 7 Files operations;

More efficient Extended Euclidean Algorithm

more symbols;

symbol interpretation for \<circle>;

update due to fontforge save operation;

moved getopts to Scala;

moved getopts to Scala;

no tracing SPAM, and thus more visible warnings;

moved getopts to Scala;

tuned messages;

more operations (like Markup.parse_bool in ML);

tuned messages;

support for command-line options as in GNU bash;

more succint formulation of membership for multisets, similar to lists; discontinued ASCII notation for multiset membership; more theorems on multisets, dropping redundant interpretation; modernized notation; some annotations concerning future work

Tuned Euclidean Rings/GCD rings

Fixed code equations for Gcd/Lcm

generalized ML function

Merged

Tuned Euclidean Ring instance for polynomials

Merged

Merged

Tuned Euclidean rings

finite precision computation to determine sign for comparison

positive precision for truncate; fixed precision for approximation of rationals; code for truncate

compute_real_of_float has not been used as code equation

tuned proof;

merged

slightly more robust re-initialization;

isabelle_scala_script is usually found by PATH;

within the Isabelle environment, main executables are always within PATH;

avoid global state change;

more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;

Merge

partial tidy-up of Sylow's theorem

proper option process_output_tail, more generous default;

Conformal_mappings: a big development in complex analysis (+ some lemmas)

tuned;

tuned signature;

proper return code for timeout (amending f868f12f9419);

retain tail out_lines as printed, but not the whole log content;

explicit class Build_Results; cancelled sessions have rc = 1 (again);

more informative Build.build_results; tuned signature;

more informative Process_Result; tuned;

clarified modules;

tuned signature;