tuned;

tuned proofs;

isabelle update_cartouches;

merged

removed dead code;

discontinued unused 'defer_recdef';

tuned;

removed dead code;

moved sources;

tuned proofs;

uniform system_mode for build test: avoid spurious output_dir/log that is not required later;

separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

generalized some theorems about integral domains and moved to HOL theories

renamed multiset_of -> mset

NEWS

multiset_of_set -> mset_set

tuned proofs -- slightly faster;

merged

tuned proofs -- slightly faster;

tuned proofs -- much faster;

tuned proofs;

tuned

merged

added funs and lemmas

tuned proofs;

merged

manual merge;

tuned proofs;

isabelle update_cartouches;

avoid dynamic parsing of hardwired strings;

more compact name

NEWS

merged

renamed Multiset.set_of to the canonical set_mset

correccted the pretty-printing specs for setsum and setprod

New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.

another messy proof fixed

merged

more informative check: dummies are always allowed parse_term and should not lead to rejection here;

vacuous fact `TERM x`;

tuned signature;

inverted another messy proof

redundant: read = check o parse;

tuned;

moved sections;

moved sections;

tuned;

more robust: variables need not occur in body;

tuned;

tuned whitespace;

merged

improved treatment of Element.Obtains via Expression.prepare_stmt; discontinued pointless all_types ctxt: prep_var is always sequential;

clarified context; tuned;

tuned comment;

another tangled proof

Merge

Tidied up more proofs

merged

more examples;

tuned signature;

tuned;

another proof

fixing more proofs

Merge

Merge

fixed another horrible proof

tuned proofs;

tuned signature;

merged

more on 'consider' and related concepts;

tuned proofs;

tuned proofs;

open parameters for 'consider' rule;

implicit rule for method "cases";

eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;

clarified 'obtain', using structured 'have' statement;

tuned comments;

clarified 'consider', using structured 'have' statement;

more examples;

renamed "prems" to "that";

support for 'consider' command; allow full "fixes" for 'obtain' command; tuned signature;

made SML/NJ happy;

support to parse obtain clause without type-checking yet; tuned signature;

tuned -- eliminated unused feature;

tuned signature;

tuned;

streamlined many more proofs

Merge

tidied more proofs

proper subclass instances for existing gcd (semi)rings

slight preference for American English

generalized euclidean ring prerequisites

simplified relationship between associated and is_unit

proof tidying

CONTRIBUTORS

tuned lemmas and proofs

given up trivial definition

dropped warnings by dropping ineffective code declarations

standardized algebraic conventions: prefer a, b, c over x, y, z

uniform _ div _ as infix syntax for ring division

fixed several "inside-out" proofs

add transfer theorems for fixed points

Merge

tidied more proofs

misc tuning;

misc tuning;

unused;

misc tuning;

isabelle update_cartouches;

more user aliases;

merged

prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;

tuned proofs;

clarified local after_qed: result is not exported yet; proper goal_export for show: 'if' is like 'assume';

support for "if prems" in local goal statements;

tuned message;

tuned proofs;

no need for protected goal (see 240ad53041c9);

tuned proofs;

prevent export of future result -- avoid interference with goal fixes;

more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;

tuned signature;

allow for_fixes for 'have', 'show' etc.; tuned signature;

eliminated dead code;

clarified abstracted term bindings (again, see c8384ff11711);

tuned signature;

tuned;

clarified term bindings;

tuned

Merge

tuned

Renaming multiset operators < ~> <#,...

more tidying up of proofs

tidying messy proofs

tidying messy proofs

merged

clarified context;

tuned;

clarified abstracted term bindings;

avoid duplicate warning due to Variable.warn_extra_tfrees;

clarified Proof_Context.cert_propp/read_propp; tuned;

more careful treatment of term bindings in 'obtain' proof body; tuned signature;

tuned signature;

Merge

Tidied lots of messy proofs

tuned signature;

tuned (see also 66e6c539a36d);

tuned signature;

clarified: declare props once and for all; tuned signature;

tuned signature;

tuned signature;

tuned signature;

tuned;

tuned;

tuned;

tuned whitespace;

more tight treatment of subgoals: main goal may refer to extra variables;

added Isar command 'supply';

tuned;

clarified signature -- better support for Isar commands outside of Pure;

merged

clarified context;

tuned;

clarified context;

cleaified context; more uniform context data; tuned;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

tuned proof;

merged

simps_of_case: Better error if split rule is not an equality

simps_of_case: allow Drule.dummy_thm as ignored split rule

implicit partial divison operation in integral domains

separate class for division operator, with particular syntax added in more specific classes

explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer

dropped dead config option

tuned, including proper signature for functor argument

dropped dead code

explicit argument expansion of uncheck rules; rewriting of user-space type system must behave similarly to abbreviations

explicit input marker for operations

completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept

self-contained formulation of abbrev for named targets

correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections

separate function to compute exported abbreviation

clearly separated target primitives (target_foo) from self-contained target operations (foo)

tuned order

dedicated config options to deactivate uncheck phase for improvable syntax

clarified interfaces for improvable syntax

tuned

clarified context;

clarified context;

clarified context;

tuned;

discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;

discontinued legacy;

obsolete (see 189c81779a68);

eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;

clarified context;

clarified context;

tuned;

clarified context;

tuned;

obsolete;

clarified context;

tuned;

tuned;

standardize towards Thm.eta_long_conversion, which just does eta_long conversion;

tuned spelling;

unused;

tuned;

more explicit context;

obsolete;

tuned -- more direct Thm.renamed_prop;

tuned message;

tuned whitespace;

removed model checks from Nitpick

document Nitpick issue

uncountability: open interval equivalences

Convex hulls: theorems about interior, etc. And a few simple lemmas.

made Auto Sledgehammer behave more like the real thing

took out Sledgehammer minimizer optimization that breaks things

modernized (slightly) type compiler in MicroJava

New material about paths, and some lemmas

removed obsolete RC tags;

merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;

Added tag Isabelle2015 for changeset 5ae2a2e74c93

clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;

updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;

tuned;

tuned;

updated versions;

tuned;

tuned;

cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;

more on displays with very high resolution;

add Haskabelle-2015 component

Added tag Isabelle2015-RC5 for changeset d7f636331176