more new theorems on real^1, matrices, etc.

a few new theorems and some fixes

new material about vec, real^1, etc.

merged

Probability builds with new definitions

Analysis builds using set_borel_measurable_def, etc.

merged

replacement of set integral abbreviations by actual definitions!

added lemma

avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle

merged

A couple of new results

Syntax for the special cases Min(A`I) and Max (A`I)

removed dots at the end of (sub)titles

moved and renamed lemmas

Added binary set operations with join-based implementation

more name tuning

better name; added binary operations

tuned

a first shot at tagging for HOL-Analysis manual

even more on bit operations

more bit operation conversions

more rules for numeral conversions; more precise code setup for pred_numeral

tuned proofs and generalized some lemmas about limits

tuned some proofs

tuned some proofs about filters

clarified handling of stdout vs. stderr: the cronjob should normally be silent;

proper self_update of components -- do assume shared file-system;

updated to scala-2.12.5;

Merged

Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)

Added some simple facts about limits

added lemmas

clarified signature;

clarified messages (amending 3e072441c96a);

session tmp_dir is default master_dir;

tuned output;

tuned;

clarified theory node name; purge_theories: return purged, retained; tuned documentation;

added lemma

added command "purge_theories"; proper documentation: command "use_theories" is asynchronous;

clarified signature -- eliminated somewhat pointless positions;

clarified signature -- more like use_theories;

clarified;

removed somewhat pointless argument;

support for purge_theories;

clarified signature;

tuned;

more robust timing info: do not rely on order of markup;

clarified signature;

field "kind" is always present, with default "writeln";

merged

eliminated "elems"

NEWS and CONTRIBUTORS

tuned;

merged

provide tmp_dir for server session;

clarified signature: flexible base_dir;

clarified exported messages, e.g. suppress "information", "tracing"; export "legacy_feature" as "warning", in accordance to console default output;

clarified signature: prefer selective include_sessions;

clarified signature: more uniform session_id;

clarified signature;

clarified signature: do not expose somewhat accidental internal options;

misc tuning and clarification;

more documentation;

clarified result;

tuned;

clarified error result, without JSON object from "session_build"; clarified regular result;

proper order of matches: Server.Error is an instance of Exn.ERROR;

clarified result;

clarified markup according to common Command.Results;

make baliL and baliR symmetric

proof of concept for algebraically founded bit lists

tuned proof

prefer convention to place operation name before type name

more lemmas

generalized

documentation for the Isabelle server;

clarified message name: disallow single quote;

clarified server shutdown: stop all sessions;

more explicit error messages; clarified signature;

more explicit errors; tuned;

additional Eisbach combinators and utility methods (by Daniel Matichuck)

fewer messages;

output result messages;

clarified signature;

more position information;

more robust check_state loop, even without session activity (e.g. idempotent use_theories);

synchronized Session.update;

more interruptible use_theories; tuned comments;

clarified exception handling: include interrupts;

support for repeated events;

tuned;

more interruptible; tuned signature;

unload_theories: actually observe required state; misc tuning and clarification;

tuned signature;

prefer typed UUID;

unload_theories after consolidation -- reset node_required; proper node_perspective (amending 0d8e4e777973);

support for "use_theories";

JSON representation for Position.T;

interruptible exploration of dependencies;

tuned signature;

clarified signature;

clarified signature;

tuned message;

proper options;

tuned options;

more comments;

tuned message -- more readable JSON;

more accurate isabelle_id: parent directory is not necessarily at tip;

store session: per Server/Context, not Connection; support for "session_stop";

clarified server log; tuned options;

support for "session_start";

updated user name;

clarified message;

clarified message;

more uniform id;

prefer non-strict defaults;

clarified default;

tuned;

asynchronous "session_build";

support for asynchronous tasks, with "cancel" command;

tuned signature;

more informative JSON results;

more informative error with JSON result; tuned signature;

tuned signature;

misc tuning and clarification;

publish current log file, e.g. for easy error detection;

more options;

allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");

tuned;

tuned signature;

merged

added server command "session_build": similar to JEdit_Resources.session_build;

tuned signature;

tuned;

more flexible preferences: avoid hardwired file; tuned signature;

tuned;

more operations for typed JSON values;

clarified signature;

clarified signature;

tuned signature; tuned output;

explicit Server.Context with output channels (concurrent write); support for Logger and Progress;

allow "." in message name;

re-use existing in/out streams;

tuned signature -- more generic;

tuned imports;

tuned;

tuned signature;

clarified signature -- do not expose socket;

Removed stray 'sledgehammer' invocation

Changes to NEWS regarding 2a6ef5ba4822

Changes to complete distributive lattices due to Viorel Preoteasa

eliminiated superfluous class semiring_bits

tuned;

tuned;

update XML cache for slightly modified messages;

more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);

more options;

clarified default server name;

more uniform output: this may be parsed by another program;

clarified argument formats: explicit Unit, allow XML.Elem as well; tuned messages: prefer single quotes for JSON output;

tuned comments;

convenience to represent XML.Body as single XML.Elem;

clarified AFP partitioning;

abstract algebraic bit operations

more balanced AFP partitioning;

workaround for occasional deadlock seen in HOL-Proofs with threads=2;

adapted to 3869b2400e22;

tuned output;

more options: client without implicit server startup;

console interaction with line-editor;

more flexible message formats;

clarified interrupt handling;

clarified signature;

option for console interaction;

more uniform Bytes.read_line/read_block operations;

auto update;

more comments;

more general TTY loop;

added Reply.NOTE for asynchronous notifications;

more operations;

more thorough init: purge inactive entries;

more generous timeout;

Entry.connection: proview password here; more robust checks;

clarified initial protocol;

ignore empty lines;

tuned;

more robust read_line after shutdown;

more implicit wire protocol;

tuned signature;

clarified server start, notably for invocation within regular Isabelle/Scala process;

tuned signature;

tuned signature;

clarified toString operations;

clarified socket connection;

server commands may access Server; Server.stop: proper shutdown; clarified signature;

tuned -- avoid regex matching on potentially large string; clarified message: command name could be malformed;

more robust build: prevent problems seen with Poly/ML eb94e2820013 on Mac OS X;

clarified notion of unknown files: ignore files outside of a Mercurial repository;

more balanced AFP partitioning;

more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

tuned -- more uniform;

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

Drop rewrite rule arguments of sublocale and interpretation implementations.

more balanced AFP partitioning;

clarified signature;

build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;

more robust: normalize potentially symbolic rev;

proxy setup for lrzcloud1;

tuned signature;

support for permissive connections, for odd situations where host keys are not accepted;

proper target directory;

eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);

document existing Apache2 configuration;

consolidated main cronjob server on virtual machine together with build_log database; eliminated special tricks for Gentoo; import plain_identify logs, export all logs for backup; run build_release, build_history_base in parallel to remote_build_history tasks;

identify closer to main cronjob -- avoid diverging changeset versions;

Drop rewrites after defines in interpretations.

proper remote_mac according to Admin/Release/CHECKLIST;

more Java heap, e.g. relevant for hg.graph on Isabelle repository;

more robust check -- do not rely on return code;

more compact ML_Statistics, to make build_status work with less than 2GB heap;

retain latest ml_stats (amending e76c6cb0d461);

accomodate smaller build machine;

clarified signature;

clarified self_update: imitate visible directory state on remote side;

more operations;

self_update implies push_isabelle_home (see also 4c253e84ae62);

uniform setup_repository (pull/clone without update); tuned signature;

clarified signature: facilitate interactive experimentation;

clarified tasks;

tuned signature;

proper order;

clarified README;

merged

more ssh options;

support for proxy connection, similar to ProxyCommand in ssh config;

prefer https;

avoid hardwired parameters; less ambitious defaults: low memory requirements;

Drop illegitimate optimisation from d5a7f2c54655.

Fall back to reading rewrite morphism first if activation fails without it.

Proper rewrite morphisms in locale instances.

clarified date for presentation vs. formal pull_date;

reveal raw data in CSV format;

support for CSV files;

tuned comment;

clarified syntax: reject formal comments explicitly, instead of ignoring them silently;

merged

generalized lemmas about orthogonal transformation

more explicit infixl (see initial 1edf0f223c6e); clarified name;

clarified use of vec type syntax;

new lemma

dedicated append function for string literals

generalized

moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

merged