tuned

avoid error in Isar proof reconstruction if no ATP proof is available

preplaying of 'smt' and 'metis' more in sync with actual method

avoid generating polymorphic SPASS constructs to monomorphic SPASS

Reorganised a huge proof

back to post-release mode -- after fork point;

merged

bypass input method for better imitation of read-only mode (cf. f26a4d5e82b5): e.g. relevant for composition of ALT-u u on Mac OS X;

tuned;

clarified -- this is available on Mac OS X, too;

updated jdk;

tuned signature (according to Scala version);

fixed NEWS w.r.t. multisets

added 'supset' variants for new '<#' etc. symbols on multisets

added lemma

tuned;

tuned;

tuned

merged

added lemma

Added approximation of powr to NEWS/CONTRIBUTORS

Made Approximation work for powr again

updated polyml;

tuned whitespace;

updated mirrors according to website;

renamed map_of to lookup

more method definitions;

tuned syntax;

tuned;

misc tuning and modernization;

keep src/Doc;

tuned URLs according to website;

more symbols;

tuned message;

tuned message;

Added tag Isabelle2016-RC1 for changeset 155d30f721dd

misc updates and tuning; more on "Output" versus "Proof state";

misc updates and tuning;

misc updates and tuning;

continuity of parameterized integral; easier-to-apply formulation of rules

tuned;

tuned;

tuned;

made SML/NJ happy;

removed dead code;

tuned syntax;

isabelle update_cartouches -c -t;

eliminated spurious Unicode;

clarified example;

updated section on "Overloaded constant definitions";

more doc content;

tuned;

removed old 'defs' command;

Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;

more doc content;

merged;

tuned signature;

proper relative symlink;

tuned;

Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);

merged

tuned layout

updated NEWS

generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes

more good NEWS;

misc tuning and modernization;

merged

updated old screenshots, added new screenshots;

more explicit errors for control symbols that are left-over after Markdown parsing;

removed in anticipation of c92d82c3f41b -- demolition after renovation;

eliminated old defs;

eliminated old defs;

clarified axiomatization versus definitions; eliminated old defs; more symbols;

eliminated old defs;

eliminated old defs;

eliminated old defs;

eliminated old defs;

eliminated old defs;

eliminated old defs;

Deleted problematic code equation in Binomial temporarily.

add reference

merged

add BNF instance for Dlist

crediting LCP in CONTRIBUTORS

more careful witness' type analysis

removed outdated example

remove unused code

remove Eisbach's dependency on HOL

match method now makes proper use of context_tactic

merged

nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.

added AA_Map; tuned titles

tuned

Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.

generalized proofs

avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables

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;