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;

identify release;

prefer Isabelle standard Path;

clarified logs;

publish directly on webspace;

Jenkins: don't build in system mode

merged

cronjob: build release from repository snapshot;

more operations;

clarified file operations;

proper link;

explicit website directory;

proper path;

tuned messages;

clarified platform families vs. bundles;

more general operations;

website index for existing bundles;

tuned messages;

added option -p for platform families; actually accept option -r;

more formal Release_Info; more incremental treatment of additional builds (bundles, library); tuned;

replaced shell script by Isabelle/Scala;

tuned;

tuned whitespace;

clarified;

tuned;

tuned message;

more robust wrt. old versions that use clear-text properties (e.g. Timing in build_history_base);

tuned;

integrity test of build_history vs. build_history_base; misc tuning and clarification;

clarified log_subdir vs. log_filename; support for sequential and parallel task blocks (unnamed);

tuned;

tuned;

provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;

tuned signature; copy_dir using *this* Isabelle_System: note that File.bash_path is already expanded, but no variables are used here;

clarified modules;

allow to exclude named tasks;

support for separate sub-system options, independent of main Isabelle options; tuned;

tuned;

tuned;

more cleanup;

separate ISABELLE_HOME_USER (with its etc/settings);

renamed lemma to a more consistent name

tuned

remove accidentally oops'ed (and wrong) lemma

transfer lifting rule for numeral

more standard naming convention

tuned;

special case for local contrib, e.g. lxbroy10;

merged

tuned signature;

tuned;

clarified task logging via log service;

more explicit management of tasks; separate logger thread with exclusive access to main.log;

tuned;

added clone_repository; tuned;

support remote repositories via ssh command execution; tuned;

tuned signature;

modernized;

separate type class for arbitrary quotient and remainder partitions

stripped dependency on pragmatic type class semiring_div

simplified: no internal state for Mercurial;

explicit indication of Admin tools;

clarified files;

explicit timezone for the sake of lxbroy10;

proper redirection;

tuned output;

tuned message -- more parsable;

tuned signature;

identify managed repository clones;

some timing and logging, similar to old isatest.log;

enforce short name, notably on Mac OS X;

tuned -- Date.Format.default used by toString;

clarified modules;

force fresh build;

basic setup for Isabelle cronjob;

tuned;

merged

build on macbroy2 for performance, but use macbroy30 for its more robust hdiutil;

makedist_bundle works on Linux as well: build dmg on remote Mac;

added isabelle remote_dmg tool;

proper type for Library.using; tuned signature;

support user@host syntax;

modernized date format;

tuned signature;

eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;

support for remote tmp dirs;

close more thoroughly;

provide execute operation, similar to Isabelle_System.bash;

proper support for exec channel (see also bash.scala);

proper hierarchic names;

more Sftp operations;

more specific channels; more Sftp operations;

clarified treatment of options; more uniform channels;

support for remote command execution; tuned;

tuned;

more generous timeout default (see also jEdit/FTP);

connect session by default; tuned signature;

clarified (hardwired!) default (see also jEdit/FTP);

tuned comment;

support for SSH in Isabelle/Scala;

invariance of domain

enforce detailed build log;

record heap sizes;

inline session ML statistics into main build log; tuned;

modernized;

build_history log files with formal meta info;

prefer explicit timezone offset for printing;

tuned;

tuned name of bit truncating operations

dedicated syntax for types with a length

merged

prefer local timezone;

support for Isabelle/Jenkins log file format;

tuned;

clarified meta info;

tuned comment;

tuned signature;

tuned signature;

more permissive: accept all historic isatest and afp-test logs;

accept spurious empty logs;

prefer static Date_Format;

more formal directory content; clarified date format;

tuned error;

tuned;

misc tuning and clarification;

clarifying NEWS file

more flexible date formats;

support for isatest format;

tuned;