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