clarified order: params/prems/concl interchangeable with !!/==> proposition;

support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;

tuned;

merged

updated subtle side-conditions;

some uses of 'obtain' with structure statement;

'obtain' supports structured statements (similar to 'define');

more portable: GNU find no longer supports "-perm +mode";

more uniform operations for structured statements;

defs are closed, which leads to proper auto_bind_facts; misc tuning;

tuned notation;

misc tuning and modernization;

Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces

Linear_Algebra: generalize linear_independent_extend to all real vector spaces

Linear_Algebra: alternative representation of linear combination

Linear_Algebra: move abstract concepts to front

merge

avoid duplicate mixfix messages in '(co)datatype' type name

generalize code to avoid making assumptions about type variable names

intermediate definitions and caching in n2m to keep terms small

n2m operates on (un)folds

clarified rendering;

old 'def' is legacy;

more rigid check of lhs;

clarified def binding position: reset for implicit/derived binding, keep for explicit binding;

eliminated old 'def'; tuned comments;

added Isar command 'define';

within a proof body context, undeclared frees are like global constants; tuned signature;

clarified modules;

added "balanced" predicate

fixed code equation for pdivmod, added improved code equation for pseudo_mod

proper latex;

merged

reactivated other_id reports (see also db929027e701, 8eda56033203);

invisible context similar to interpretation;

avoid massive multiplication of reports due to interpretation;

tuned comments;

more thorough update;

several updates on polynomial long division and pseudo division - division of polynomials is now available on idom_divide (was field before) - added polynomial pseudo division (on comm_ring_1) - improved code equation for polynomial (pseudo)-division (joint work of S. Joosten, R. Thiemann, and A. Yamada)

fragment of a HOL type class primer

capitalized GCD and LCM syntax

environment variable check has become pointless after 771b8ad5c7fc

unfold internal definitions before emitting a proof obligation

more IDE support for Isabelle/Pure bootstrap;

merged

tuned signature;

prefer internal attribute source;

tidying some proofs; getting rid of "nonempty_witness"

Merge

numerous theorems about affine hulls, hyperplanes, etc.

merged

proper LaTeX;

tuned;

clarified bindings;

clarified bindings;

tuned;

tuned;

avoid clash with function called "x";

new theorems about convex hulls, etc.; also, renamed some theorems

clarified bindings;

clarified bindings;

prefer binding over base name;

clarified signature;

removed pointless check (see Type_Infer.object_logic);

prefer precise names for internal construction;

remove "slow" session tags

misc tuning and modernization;

clarified reported positions;

operate on proper binding; tuned;

tuned;

add "slow" group to descendants of HOL-Proofs

merged

support for Poly/ML entity ids;

clarified PIDE reports;

clarified rendering wrt. hyperlinks;

tuned -- no position;

clarified focus visibility;

tuned rendering;

highlighting of entity def/ref positions wrt. cursor;

background color for entity def/ref focus;

tuned;

more silence;

avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;

tuned;

tuned;

clarified context;

misc tuning and standardization;

tuned headers;

fix HOL-Probability-ex

change is incompatible

Probability: move emeasure and nn_integral from ereal to ennreal

tuned;

clarified modules;

tuned;

back to exact copy of non-text file (amending dcc8e1d34b18); explicit chmod, since Files.copy appears to copy permissions regardless of StandardCopyOption.COPY_ATTRIBUTES;

merged