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;

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;