tuned signature;

support for Poly/ML heap hierarchy, which saves a lot of disk space;

clarified signature;

tuned signature;

less physical "logic" argument, with option -l like "isabelle console" etc.;

find heaps uniformly via Sessions.Store; tuned;

clarified modules;

clarified modules;

ML save_state under control of Isabelle/Scala;

clarified prompt: "ML" usually means Isabelle/ML;

record stamps of cumulative input heaps; tuned;

Merge

Contractible sets. Also removal of obsolete theorems and refactoring

add measurability rules for ennreal

generalized some Borel measurable statements to support ennreal

rationalisation of theorem names esp about "real Archimedian" etc.

add fixpoint induction principle

generalized ML function

New results about paths, segments, etc. The notion of simply_connected.

Merge

Refactoring (moving theorems into better locations), plus a bit of new material

strengthened tactics

tuned;

tuned signature;

prefer Scala over bash function;

tuned;

clarified env;

unused;

more uniform signature for various process invocations; env refers to full environment, not the update;

tuned;

more theorems on orderings

dropped junk

tuned;

merged

tuned;

clarified cleanup;

more thorough cleanup -- in Scala;

create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);

obsolete (cf. 63a5782c764e);

clarified session build options: already provided by ML_Process; tuned signature;

spelling

model characters directly as range 0..255 * * * operate on syntax terms rather than asts

tuned messages;

tuned message;

generate theorems like 'bool.split_sel'

merged

tuned;

tuned;

upgrade "isabelle build" to Isabelle/Scala;

prefer plain "isabelle" from PATH within Isabelle settings environment;

isabelle_process is superseded by "isabelle process" tool; tuned tool usage; misc updates and tuning of "system" manual;

clarified messages, notably on Windows where CPU time of poly.exe is not measured;

clarified modules;

clarified files;

clarified files;

don't throw an exception when trying to print an error message

eta-expansion done right in "primcorec"

clarified: constructors in the sense of the code generator are not invertible; correct treatment of constructors with same name but different type; moved doubtful comment to corresponding function call

moved

merged

obsolete;

clarified interactive mode, which is relevant for ML prompts;

more careful print_depth on startup;

ignore SIGINT in waiting wrapper process; proper "bash_process.c" and "build" within component;

more robust cleanup; more defensive timing value;

isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");

tuned;

print timing like lib/scripts/timestop.bash;

prefer explicit locale;

bash process with builtin timing;

elapsed time in milliseconds (cf. Time.now in Poly/ML);

support for timing of the managed process;

tuned;

proper support for RAW_ML_SYSTEM;

tuned signature;

separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";

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

ignore execeptions that usually occur due to shutdown;

clarified initial ML;

isabelle console is based on Isabelle/Scala;

clarified process interrupt: exactly one signal (like thread interrupt);

tuned signature;

more abstract Session.start, without prover command-line; Isabelle_Process.apply is directly based on ML_Process; clarified Isabelle_Process.main command-line; tuned signature;

removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;

prospective command line entry point for simplified isabelle_process;

tuned signature;

proper Path.print for user messages;

discontinued cd, pwd;

tuned -- more standard operations;

File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;

clarified treatment of DEL; tuned signature;

clarified RAW_ML_SYSTEM;

tuned;

Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined; more robust File.bash_escape; more robust treatment of ML_OPTIONS; clarified prover args (again);

manage the underlying ML process in Scala;

clarified modules;

tuned signature;

Merge

Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem

explicit record values for dictionary variables

provide explicit hint concering uniqueness of derivation

syntax for multiset membership modelled after syntax for set membership

made 'size' plugin compatible with locales again (and added regression test)

strengthened tactic

complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)

new material to Blochj's theorem, as well as supporting lemmas

merged

less resetting of local theories

avoid redundant escapes;

clarified treatment of fragments of Isabelle symbols during bootstrap;

clarified ML syntax for strings concerning UTF8;

tuned signature;

tuned

NEWS after Isabelle2016;

proper latex setup;

tuned;

abbreviations for \<nexists>;

old HOL syntax is for input only;

more PIDE markup;

tuned signature -- clarified modules;