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;

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;

merged

accept obscure timezone used in 2011;

more liberal parsing for old AFP logs;

more operations;

more permissive timing data;

more permissive for old logs;

more uniform regexps;

clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);

clarified parse_build_info: isabelle build output; clarified Session_Status; tuned signature;

more operations;

more operations;

clarified signature;

more uniform treatment of settings;

clarified modules; CI_Profile: show all settings;

tuned;

more official legacy status;

more lemmas

tuning multisets

more lemmas

Set_Permutations -> Multiset_Permutations in NEWS

moved to proper release (cf. 4a72b37ac4b8); tuned;

updated for release;

merged

Added tag Isabelle2016-1-RC0 for changeset 666c7475f4f7

merged

merged

less aggressive unfolding in tactic

merged

moved lemmas

merged

tuned signature;

misc tuning and clarification;

some support for header and data fields, notably from afp-test;

tuned signature;

more flexibile formatting; expose representation for free-form formatters;

proper calculation;

more operations; tuned;

more date and time operations from Java 8;

proper imports;

clarified modules;

more operations;

added multicore_base option;

allow multiple threads configurations;

tuned;

misc tuning and clarification;

clean output dir for fresh rebuild; clarified echo;

allow multiline script;

clarified sanity checks;

clarified modules;

historic workaround according to 22630327408b;

more thorought update of components;

check session name;

tuned signature;

tuned error;

earlier build_history_base: timing properties in log are introduced here;

incremental output; tuned;

clarified output;

clarified heap options;

proper ISABELLE_TOOL_JAVA_OPTIONS (as in "isabelle" wrapper);

more ambitious default as in former isatest;

tuned signature;

tuned;

more sanity checks;

more options for generated settings;

more robust build_history_base;

more robust;

proper log output;

clarified command line; clarified result;

clarified command-line; init settings and components;

more operations;

more formal build_history_base;

clarified cold-start environment;

basic setup for Admin/build_history -- outside of Isabelle environment;

clarified: a variant of -i is the default, but its output is not as precise as it might seem;

merged

replaced floorlog by floor/ceiling(log .)

more multiset simp rules

tuned proof -- much faster

proof of concept for algebraically founded word types

more lemmas

option to report results of solve_direct as explicit warnings

modernized option

CONTRIBUTORS

Probability: move some theorems from AFP/Density_Compiler

Probability: variant of central limit theorem with non-zero mean

HOL-Probability: more about probability, prepare for Markov processes in the AFP

Merge

new theorems including the theory FurtherTopology

clarified magic values (see also java/io/BufferedInputStream.java);

clarified stream operations; added XZ data compression;

tuned signature;

clarified modules; afford explicit string composition in terminate_lines;

more general read_stream: return actual byte count;

clarified modules;

more operations;

more operations;

more formal Mercurial support (with the potential to upgrade to command server);

tuned whitespace;

added isabelle_java cold-start executable;

updated according to 85c83757788c;

eliminated hard tabs;

updated headers;

updated to sumatra_pdf-3.1.2;

updated to xz-java-1.5;

updated cygwin according to 9416333a17c2, still using old 1.7.35-1;

tuned;

just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;

options for process policy, notably for multiprocessor machines;

tuned;

tuned messages -- facilitate copy-paste;

merged

tuned;

tuned proofs;

Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);

clarified lfp/gfp statements and proofs;

repair LaTeX

misc tuning for release;

added lemma;

Trying out "subgoal", and no more [| |]

HOL-Analysis: fix latex generation

Probability: fix proof

Library: fix name Product_plus to Product_Plus

HOL-Analysis: move Product_Vector and Inner_Product from Library

HOL-Analysis: move Continuum_Not_Denumerable from Library

HOL-Analysis: move Library/Convex to Convex_Euclidean_Space

HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)

new material on paths, etc. Also rationalisation

Merged

Set_Permutations replaced by more general Multiset_Permutations

CONTRIBUTORS: new proof method "argo"

NEWS: new proof method "argo"

use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable

invoke argo as part of the tried automatic proof methods

new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic

HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)

HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure

HOL-Analysis: move gauges and (tagged) divisions to its own theory file

HOL-Analysis: add cover lemma ported by L. C. Paulson