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;