tuned document;

more proofs;

tuned;

more notation; more examples;

clarified sessions;

tuned;

isabelle update_cartouches -c -t;

misc tuning and modernization;

more proofs, more text;

modernized example;

tuned proofs and augmented lemmas

tuned proof

less ambitious test;

tuned;

clarified directory structure;

updated polyml;

clarified context policy to allow multiple dummies;

NEWS;

tuned;

merged

tuned module arrangement;

tuned module arrangement;

check and report source at most once, notably in body of "match" method;

transfer rule for bounded_linear of blinfun

theory for type of bounded linear functions; differentiation under the integral sign

stripped some legacy

tuned proofs and augmented some lemmas

more standard nesting of sub-language: Parse.text allows atomic entities without quotes;

proper full name within the name space of the method definition;

tuned signature; tuned;

isabelle update_cartouches -c -t;

Merge

Liouville theorem, Fundamental Theorem of Algebra, etc.

Weierstrass: whitespace

merged

more thorough event propagation;

tuned -- with subtle change of order of evaluation;

more accurate lookup of dynamic facts;

tuned;

tuned;

tuned signature;

tuned;

Bochner integral: prove dominated convergence at_top

dead code;

tuned spelling; tuned white-space;

merged

misc tuning and modernization;

merged

documentation on last state of the art concerning interpretation

abandoned attempt to unify sublocale and interpretation into global theories

updated Cygwin (somewhere after 1.7.35-1);

merged

merged

tuned message;

more explicit ML profiling, with official Isabelle output;

discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);

clarified length of block with pre-existant forced breaks;

Probability: fix coercions (real ~> real_of_enat)

Transcendental: use [simp]-canonical form - (pi/2)

moved some theorems from the CLT proof; reordered some theorems / notation

tuned whitespace;

tuned signature;

renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;

proper formatting via Pretty.string_of; tuned;

unused;

tuned;

prune old document versions more frequently, for reduced heap usage;

merged

more explicit Pretty.Tree, like in ML; tuned;

tuned;

clarified underlying datatypes;

tuned;

prefer default focus policy, like Output dockable;

tuned;

tuned signature;

support for blocks with consistent breaks; tuned;

preserve break indentation;

support pretty break indent, like underlying ML systems;

register record functions as 'Spec_Rules'

cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer

removed subsumed dependency

removed dead code

add serialisation for abs on integer to target language operation

add gcd instance for integer and serialisation to target language operations

merged

tuned whitespace;

rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

tuned signature -- clarified modules;

unused;

unused;

Merge

New complex analysis material

infix syntax for measurable set

more standard term equality;

tuned;

tuned signature;

tuned message;

merged

more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;

tuned;

clarified ML scopes; tuned;

clarified ML scopes;

tuned;

unused;

tuned;

clarified modules;

modernized

modernized

modernized

isabelle update_cartouches -c -t;

proper checksum for cygwin-20151210.tar.gz (some snapshot after 1.7.35-1);

avoid application spurious startup error;

current Cygwin snapshot in preparation of release;

hardwired LANG, to avoid sporadic surprises with local environments;

make SML/NJ happy;

not_leE -> not_le_imp_less and other tidying

clarified terminology

tuned;

tuned signature;

tuned signature;

tuned;

more direct use of Token.src as token list; tuned signature; tuned;

merged

unused;

merged

clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;

tuned;

tuned;