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

more new material

Generalised the type of map_poly

Merge

new material connected with HOL Light measure theory, plus more rationalisation

sequential (jobs = 1) makeall profile

syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div

dropped tautological pattern

more warning comments

more lemmas

spelling

a few new theorems and a renaming

use filter to define Henstock-Kurzweil integration

include generation time in statistics

CI script to generate timing statistics

move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral

prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions

Merge

More mainly topological results

merged

discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;

raw control symbols are superseded by Latex.embed_raw;

\<^raw> output is intended for LaTeX;

more general mixfix delimiters;

more tight implementation of symbol explode operation (without support for raw symbols);

approximation: preprocessing for nat/int expressions

provide more information on error

approximation: rewrite for reduction to base expressions

new material about topological concepts, etc

vector_add_divide_simps now a "named theorems" bundle

tuned -- fewer warnings;

avoid old SML90;

more generic algebraic lemmas

NEWS: Normalized_Fraction.thy

Merged

Additions to permutations (contributed by Lukas Bulwahn)

resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet

# after multiset intersection and union symbol

left_distrib ~> distrib_right, right_distrib ~> distrib_left

tuned;

merged

tuned proofs;

merged

tuned

clarified notation: iterated quantifier is negated as one chunk;

tuned proofs;

tuned;

clarified notation;

support replicate_mset in multiset simproc

tuning multiset simproc

repair LaTeX dropout from f83ef97d8d7d

prefer abbreviation for trivial set conversion

more lemmas

merged

more symbols -- as in the printed document;

more symbols;

tuned proofs

misc updates;

merged

consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;

merged

Liminf/Limsup and filtermap

benchmark doesn't need to build documents

benchmark profile runs on small worker now (6 cores)

merged

NEWS

merged

serious measurements require jobs = 1;

sessions that are relevant for routine timing measurements;

more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);

move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel

new type for finite maps; use it in HOL-Probability

adapted to listsum -> sum_list

merged

renamed listsum -> sum_list, listprod ~> prod_list

lots of new results about topology, affine dimension etc

Merge

simple new lemmas, mostly about sets

add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set

tuned;

merged

NEWS;

handle font-size events;

clarified GUI representation of replacement texts with zero or more abbrevs;

handle update events; tuned;

discontinued global etc/abbrevs;

added abbrevs panel;

tuned;

more robust;

maintain abbrevs in canonical reverse order;

tuned;

tuned;

ignore default output directory of 'build_stats' tool

don't expose internal construction in the coinduction rule for mutual coinductive predicates

union associates to the left

reorganization, more funs and lemmas

more lemmas

make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions

tuned;

tuned -- fewer warnings;

moved ML function

NEWS

strengthened tactic

avoid warning triggered by code generator

strengthened tactic

prove 'set' property backward

more robust multiset simproc

delete looping simp rule

merged

tuned proofs;

tuned proofs;

generalized code towards nonuniform (co)datatypes

merged

more simp rules

strengthened tactics

derive relator properties forward

derive maps forward

tuning

tuning

provide a mechanism for ensuring dead type variables occur in typedef if desired

preserve order of dead variables

tuning

tuned proofs;

misc tuning and modernization;

misc tuning and modernization;

more simp

msetsum -> set_mset, msetprod -> prod_mset

More on balancing; renamed theory to Balance

added lemmas

option "checkpoint" helps to fine-tune global heap space management;

made it easier to catch 'empty datatype' exception

export ML functions

tuning

minimal HTTP server;

merged

unfold_abs_def is enabled by default;

discontinued theory-local special syntax for lattice orderings

keep locale lifting rules on the global level

tuning

exported ML functions + tuning

refactoring

refactoring

refactoring

tuned whitespace

merged

more operations;

clarified proof: save 1-2s CPU time;

tuned;

strictly sequential abbrevs;

clarified obscure facts;

clarified modules;

clarified modules;

standardized alias;

export more ML functions

generalized ML signature

extended ML signature + refactored

extended ML signature

generalized code (subtly)

tuned ML signature

exported ML functions

export ML function + tuning

tuning multisets; more interpretations

clean argument of simp add

add_mset constructor in multisets

merged

more operations;

more operations; tuned;

support resource management;

clarified modules;

export more ML functions

export more ML functions

added warning

tuned;

tuned signature;

clarified exceptions;

support for (single) primary key; more operations;

more operations; clarified NULL treatment;

more operations;

clarified modules; tuned signature;

tuned;

minimal support for SQLite databases;

merged

make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;

simplified;

tuned;

merged

added lemmas

consider equality proxy in monotonicity analysis

adapted remote E

Merged

Some facts about factorial and binomial coefficients

added inorder2

tuned headers;

clarified session: use all theories in directory HOL/Library;

clarified session; misc tuning and modernization;

more careful quoting, e.g. relevant for \<^control>cartouche;

uniform capitalization of labels;

tuned message;

merged

avoid conflict after initial keymap migration;

merged

Renamed balanced to complete; added balanced; more about both

tuned GUI: modal dialog last;

tuned message;

merged

NEWS;

more robust persistent storage; tuned;

clarified important directories;

separate action; tuned message;

check keymap changes on startup;

tuned message;

clarified GUI; tuned;

actual actions; tuned;

tuned;

clarified;

tuned GUI;

clarified GUI;

tuned GUI;

tuned rendering;

more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;

clarified shortcut conflicts; tuned;

clarified (see 019856db2bb6, ea52509f4c42);

some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;

added glyph from "Deja Vu Sans Mono" font;

more robustness

added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)

make workaround possible for Quickcheck with nesting

tuned docs

tuned final stop in message

generate proper goal when equation is entered programmatically

clarified default;

Bohr-Mollerup theorem for the Gamma function

Back to original example theorem.

Improved error reporting when activating a locale instance.

Deprivatisation of lemmas in Polynomial_Factorial

More analysis lemmas

added lemma