tuning

exported ML function

setup code generation for filters as suggested by Florian

merged

filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones

isar-ref entry for print_record

add more frequently-run test for print_record

print_record NEWS and CONTRIBUTORS

print_record: diagnostic printing of record definitions

misc tuning and modernization;

prune old versions more often, to reduce overall heap requirements;

generate HTML version of NEWS, with proper symbol rendering;

tuned -- according to ML version;

suppress somewhat pointless description (NB: this is displayed in 'print_methods');

merged

tuned syntax;

tuned;

\<struct> loses its rendering and is superseded by \<diamondop>; tuned;

discontinued \<struct> syntax;

tuned whitespace;

tuned;

clarified symbol insertion, depending on buffer encoding;

tuned;

fix code generation for uniformity: uniformity is a non-computable pure data.

add uniform spaces

merged

merged

tuned;

merged

more uniform treatment of symblinks: avoid confusion when unpacking .tar.gz bundle with NTFS links;

tuned signature;

prefer non-ASCII output;

more uniform treatment of package internals;

more thorough GUI update;

tuned;

added lemma

Tuned constant approximations

merged

revisions to limits and derivatives, plus new lemmas

Added formal power series updates to NEWS/CONTRIBUTORS

Tuned approximations in Multivariate_Analysis

misc tuning for release;

add the proof of the central limit theorem

nicer 'Spec_Rules' for size function

updated docs

updated NEWS

more complete setup for 'Rat' in Nitpick

more systematic treatment of dynamic facts, when forming closure;

clarified ROOT files;

proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;

added ML antiquotation @{method};

tuned;

tuned;

isabelle update_cartouches -c -t;

merged

more realistic Eisbach method invocation from ML; misc tuning and clarification;

unused;

more robust event propagation;

Fixed sectioning in HOL/Library/Polynomial

Merged

Added some facts about polynomials

misc tuning for release;

merged

fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;

tuned;

Added summability/Gamma/etc. to NEWS and CONTRIBUTORS

proper latex setup;

updated headers;

merged

ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;

Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)

merged

tuned proofs;

node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;

stop dummy sessions as well;

clarified order of shutdown;

Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function

retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);

proper treatment of RAW bootstrap session;

tuned whitespace;

more symbols; tuned;

tuned spacing of \<partial>; spontaneous update of .sfd files due to fontforge;

eliminated somewhat pointless and obscure options;

isabelle update_cartouches -c -t;

tuned;

proper platform_path for Windows;

clarified isabelle jedit command-line;

tuned;

avoid downloading contrib again;

provide server name uniformly on all platforms;

more symbols;

NEWS;

keep platform bundle for reference, e.g. for headless installation;

keep generic archive for all platforms -- required for Admin/Release/build_library;

oops;

Added tag Isabelle2016-RC0 for changeset e18444532fce

tuned;

updated for release;

tuned;

more symbols;

clarified abbrev;

clarified meaning of \<^bold> action, depending on group;

clarified groups, notably for Symbols dockable;

glyphs for \<bind>, \<then>;

tuned order for isar-ref;

isabelle update_cartouches -c -t;

updated for release;

updated to SML/NJ 110.79;

misc tuning for release;

misc updates for release;

expand hard tabs;

documentation for "isabelle jedit_client";

discontinued documentation of old browser; tuned;

more precise context -- potentially relevant for Eisbach dummy thm;

tuned;

updated sumatra_pdf;

clarified imports;

clarified directory structure;

updated isabelle_fonts;

proper diamond from lasy10;

modernized defs; tuned proofs; tuned whitespace;

more symbols;

more symbols;

isabelle update_cartouches -c -t;

more symbols;

more symbols;

more symbols;

clarified print modes;

updated print modes;

modernized Isabelle document markup;

clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms; more standard spacing for big operators;

clarified print modes; more symbols;

more symbols;

more symbols;

removed junk;

more symbols;

clarified print modes;

clarified print modes;

clarified print modes; more symbols;

isabelle update_cartouches -c -t;

clarified print modes;

more symbols;

more symbols;

more symbols;

more symbols;

clarified syntax;

clarified print modes;

proper latex setup;

proper latex setup;

more symbols;

isabelle update_cartouches -c -t;

tuned java options;

more symbols;

simplified abbrevs: exploit ambiguity;

more symbols;

more symbols;

more symbols;

avoid immediate completion as ASCII versions that are still used;

tuned order for isar-ref manual;

more symbols;

updated isabelle_fonts;

more arrow symbols;

more arrow symbols;

eliminated obscure macro that is in conflict with amsmath.sty;

more abbrevs;

support additional abbrevs;

tuned;

isabelle console: print mode "ASCII";

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; uniform syntax for Pure.imp; removed obsolete "HTML" syntax;

more symbols;

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

more symbols;

use symbols by default;

prefer symbols for "Union", "Inter";

clarified position information;

suppress irrelevant position reports;

suppress irrelevant position reports;

tuned;

more position information;

put example into separate session, to restrict precious session image to library theories

more symbols;

prefer symbols for "abs";

discontinued ASCII replacement syntax <*>;

prefer symbols for "floor", "ceiling";

discontinued ASCII replacement syntax <->;

more symbols;

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;