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;

avoid deprecated Scala;

minor updates after fresh installation of virtual Windows 2012: retain old versions of mingw for this brittle build process;

misc tuning and updates;

clarified default args; more ambitious tests;

speculative support for latest Mac OS X versions -- no reference systems yet;

merged

more ambitious default;

updated to new structure Foreign; more robust memory management;

HOL-Probability: Essential Supremum as Limsup over ae_filter

less ambitious test;

proper type for Poly/ML development version;

more operations;

more on sgn in linear ordered fields

merged

test for Windows/Cygwin;

extra trim_line for the sake of Windows;

prevent sporadic disconnection;

check Windows file names, e.g. relavant for native Mercurial, but also for Isabelle/Scala;

tuned

NEWS

HOL-Probability: generalize theorems about cumulative distribution function

HOL-Probability: move stopping time from AFP/Markov_Models

HOL-Probability: generalize type of essential supremum

Repaired LaTeX in HOL-Data_Structures

More on Fibonacci numbers

build HTML library in Isabelle/Scala;

proper echo; tuned;

more robust bootstrap, e.g. when experimenting with Poly/ML repository changes;

updated to jdk-8u112;

basic SSH server configuration;

proper isabelle tool in Scala;

tuned;

merged

added system option "profiling";

replaced inefficient valid_accesses by is_valid_access, based on stored input accesses: e.g. relevant for Proof_Context.update_thms;

tuned signature, in accordance to Isabelle_System;

tuned;

clarified modules;

another attempt to squeeze a list into a property list entry;

report actual build_args;

more flexible multicore configuration;

clarified multiple props: result needs to fit on a single line within the log file;

clarified properties;

tuned;

support for free-form build tags; tuned;

explicit identification of builds and correlated build groups;

avoid spamming log file;

shared_home is default for classic isatest home setup; distinct ISABELLE_IDENTIFIER for all tasks;

add missing file Essential_Supremum.thy

Merge

Inserted necessary dependency

suitable logical type class for abs, sgn

HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp

Merge

more from moretop.ml

Jenkins: build in system mode again (backout of 3dbfd6758735)

Jenkins: configurable clean build

HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory

HOL-Probability: move conditional expectation from AFP/Ergodic_Theory

Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)

restored document structure after theory refactoring

NEWS; tuned comment;

merged

merged

improved platform coverage: macbroy30, macbroy31; slightly improved performance on lxbroy10;

eliminated unused argument;

accomodate Poly/ML repository version, which treats singleton strings as boxed;

re-use "threads" for --gcthreads;

merged

setprod -> prod

merged

Modified transfer principle in HOL/NSA to cause less ho-unficiation

merged

updated to setsum -> sum

setsum -> sum

uniform Isabelle settings -- avoid picking up different JAVA_HOME;

isabelle build -N;

support for Non-Uniform Memory Access of separate CPU nodes;

proper result;

merged

merged

more thorough cleanup;

tuned;

removed useless operation -- would require bash_process wrapper;

tuned signature;

simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;

more robust;

sftp.mkdirs according to 2a5dbad75355;

more compression for big log files;

clarified setup_repository: more uniform pull vs. clone, without update;

proper setup of fresh repository;

clarified prover-specific rules

dropped potentially explosive rule for groebner simpset, with no observable effect on examples

simplified fact references

avoid effectively subsumed rules; simplified fact reference

eliminated irregular aliasses

avoid references to lemmas designed for prover tools

clarified theorem names

eliminated irregular aliasses

more standardized theorem names for facts involving the div and mod identity

transfer rules for divides relation on integer and natural

more standardized names

added lemma

de-orphanized declaration

tuned;

discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;

timeout as in former isatest-makeall;

more robust quasi-unique name;

clarified signature: more static types;

clarified hg.id operation, with explicit tip as default;

added remote_build_history tasks: parallel on several remote hosts; isabelle_identify: use self repos for robustness; more logger context: options and ssh; setup repository clones on demand; clarified target repositories;

added setup_repository; clarified root: expanded in target environment;

more operations;

expand relatively to given environment, notably remote HOME;

tuned;

tuned signature;

tuned;

clarified treatment of non-text bytes;

remove invocation of build_history: results are reported via stdout;

clarified signature;