disable CVC4 statistics, and hence crashes upon user interruptions

back to stable scala-2.11.8;

self_update of components, e.g. for vmnipkow9;

updated to scala-2.12.0;

tuned

more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');

extra newline as for other tools;

prefer standard_path for bash arg;

ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala);

proper remote repository source;

clarified setup_repository: even more uniform pull vs. clone (see also e84cba30d7ff);

pull isabelle-release;

Merged natlog2 into Discrete.log

moved IMP/Abs_Int_ITP to AFP/Abs_Int_ITP2012

added lemma

added simp rule

generalized experimental feature slightly

provided more efficient interface

back to stable scala-2.11.8;

updated to scala-2.12.0;

tuned

tuned signature

back to post-release mode -- after fork point;

tuned;

updated to new cronjob;

build_release on lxbroy10 appears to work, including latex and remote_dmg;

misc tuning and modernization;

always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)

moved contribution to right release

more explicit pull;

types to sets: initial commit

avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar

adapted Nunchaku integration to keyword renaming

tuned;

merged

Added tag Isabelle2016-1-RC1 for changeset 9ee2480d10b7

a more general relator domain rule for the function type

Haskabelle is presently unmaintained;

tuned;

merged

more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;

avoid multiple PIDE markup due to (potentially infinite) backtracking;

more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;

more lemmas

updated CVC4 component

tuning

more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)

added lemma

tuning

preprocess typedefs and quotients correctly

adapted Nunchaku's input syntax to new design decisions

more informative error (see 6e9c22c494c5);

tuned signature -- more friendly for experimentation;

clarified hg push return code: 1 means "nothing to push";

proper Nunchaku setup to use CVC4 and Kodkod

more specific hardware information: relevant for ultimate Mac OS X version;

just one task to identify Isabelle + AFP repository snapshots and build release; report AFP changeset id on website;

tuned;

Deleted spurious markup

latest Mac OS X versions *are* still supported, but presently without formal reference systems;

pagecolor no longer exists; uniform use of pdfpagelabels (see 790f73fa8b36);

merged

use other remote_mac: macbroy30 is down;

more robust printing of names in the context of outer syntax;

more informative error (stderr);

more new material

Merge

more new material

tuned and updated for release;

updated for release;

tuned;

misc tuning for release;

added Nunchaku integration

merged

version provided by web server;

proper default Windows ACLs, e.g. relevant when the bundle is placed into the root directory of a volume;

unused;

tuned documentation

document limitations

more accurate error message

robustness

document transfer_prover_eq and friend_of_corec_simps

additional user-specified simp (naturality) rules used in friend_of_corec

apply transfer_prover after folding relator_eq

merged

more thorough cleanup of lib/classes -- it may contain broken Pure.jar or copies of Scala libraries (in historic versions);

remove old target: it is on the classpath and may break scalac;

updated to cygwin-20161024: cygwin.exe from current http://isabelle.in.tum.de/cygwin_2016-1

retain Admin component for isabelle tool invocation;

tuned;

more robust;

discontinued unused / untested distinction of separate PIDE modules;

proper Admin tool;

tuned message;

updated for release;

updated to jedit_build-20161024: Code2HTML 0.7, Navigator 2.7;

Merge

"subgoal" examples

Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory

more readable output: whitespace is insignificant in HTML;

misc tuning and clarification;

modernized;

more operations;

more operations (see also properties.ML);

tuned signature: avoid conflict with "paragraph" as section heading;

tuned;

support for XML as HTML; tuned;

tuned;

more explicit rev (tip);

just one output file;

more tasks; clarified default args;

remote_builds has PAR-SEQ semantics of old isatest-makedist; tuned signature;

expose results on failure (via mail);

clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);

support for URL notation;

process results immediately;

permissive rename operation (amending b265dd04d57d);

pro-forma update to cygwin_2016-1 (web service still missing);

updated to current Cygwin, after 2.6.0-1 from 31-Aug-2016;

regular user tool;