renamed prefix* in Library/Sublist

generate Vampire 4.0 compatible output

Merge

Lots of new material for multivariate analysis

removed odd cases rule (see also 8cb42cd97579);

tuned proofs;

tuned document;

misc tuning and modernization;

proper document source; tuned proofs;

misc tuning and modernization;

merged

added timing lemmas

uniformly continuous function extended continuously on closure

reduce isUCont to uniformly_continuous_on

removed smt proof

better handling of veriT's 'unknown' status

Resolved name clash

Merged

Moved material from AFP/Randomised_Social_Choice to distribution

Library: add partition_on

proper consideration of chained facts in 'try0' minimization

re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);

tuned;

toplevel theorem statements support 'if'/'for' eigen-context;

reverted accidental commit;

eliminated use of empty "assms";

more complete theories;

common entity definitions within a global or local theory context;

clarified heading

a quasi-recursive characterization of the multiset order (by Christian Sternagel)

merged

avoid spurious fact index, notably in "context begin" (via Bundle.context);

tuned;

tuned;

tuned;

expose Sessions.Info in Build.Results

introduced class topological_group between topological_monoid and real_normed_vector

find dynamic facts as well, but static ones are preferred; tuned;

some slight generalizations

Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman Minkowski theorem

two new lemmas about segments

Merge

lemmas about dimension, hyperplanes, span, etc.

merged

clarified context, notably for internal use of Simplifier;

renamings and refinements

move Stirling numbers from AFP/Discrete_Summation

the standard While-rule

re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;

unfold is subject to unfold_abs_def (still inactive); tuned signature;

tuned;

NEWS;

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;