2016-05-23 wenzelm 2016-05-23 misc tuning and modernization;
2016-05-23 wenzelm 2016-05-23 proper document source; tuned proofs;
2016-05-23 wenzelm 2016-05-23 misc tuning and modernization;
2016-05-21 nipkow 2016-05-21 merged
2016-05-21 nipkow 2016-05-21 added timing lemmas
2016-05-20 immler 2016-05-20 uniformly continuous function extended continuously on closure
2016-05-20 immler 2016-05-20 reduce isUCont to uniformly_continuous_on
2016-05-20 immler 2016-05-20 removed smt proof
2016-05-20 fleury 2016-05-20 better handling of veriT's 'unknown' status
2016-05-18 Manuel Eberl 2016-05-18 Resolved name clash
2016-05-17 eberlm 2016-05-17 Merged
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-17 hoelzl 2016-05-17 Library: add partition_on
2016-05-17 blanchet 2016-05-17 proper consideration of chained facts in 'try0' minimization
2016-05-14 wenzelm 2016-05-14 re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
2016-05-14 wenzelm 2016-05-14 tuned;
2016-05-14 wenzelm 2016-05-14 toplevel theorem statements support 'if'/'for' eigen-context;
2016-05-14 wenzelm 2016-05-14 reverted accidental commit;
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-05-13 wenzelm 2016-05-13 more complete theories;
2016-05-12 wenzelm 2016-05-12 common entity definitions within a global or local theory context;
2016-05-12 haftmann 2016-05-12 clarified heading
2016-05-12 haftmann 2016-05-12 a quasi-recursive characterization of the multiset order (by Christian Sternagel)
2016-05-12 wenzelm 2016-05-12 merged
2016-05-12 wenzelm 2016-05-12 avoid spurious fact index, notably in "context begin" (via Bundle.context);
2016-05-12 wenzelm 2016-05-12 tuned;
2016-05-12 wenzelm 2016-05-12 tuned;
2016-05-12 wenzelm 2016-05-12 tuned;
2016-05-12 Lars Hupel 2016-05-12 expose Sessions.Info in Build.Results
2016-05-11 immler 2016-05-11 introduced class topological_group between topological_monoid and real_normed_vector
2016-05-10 wenzelm 2016-05-10 find dynamic facts as well, but static ones are preferred; tuned;
2016-05-10 immler 2016-05-10 some slight generalizations
2016-05-10 paulson 2016-05-10 Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman Minkowski theorem
2016-05-10 paulson 2016-05-10 two new lemmas about segments
2016-05-09 paulson 2016-05-09 Merge
2016-05-09 paulson 2016-05-09 lemmas about dimension, hyperplanes, span, etc.
2016-05-09 wenzelm 2016-05-09 merged
2016-05-09 wenzelm 2016-05-09 clarified context, notably for internal use of Simplifier;
2016-05-09 paulson 2016-05-09 renamings and refinements
2016-05-04 hoelzl 2016-05-04 move Stirling numbers from AFP/Discrete_Summation
2016-05-01 nipkow 2016-05-01 the standard While-rule
2016-04-29 wenzelm 2016-04-29 re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
2016-04-28 wenzelm 2016-04-28 unfold is subject to unfold_abs_def (still inactive); tuned signature;
2016-04-28 wenzelm 2016-04-28 tuned;
2016-04-28 wenzelm 2016-04-28 NEWS;
2016-04-28 wenzelm 2016-04-28 clarified order: params/prems/concl interchangeable with !!/==> proposition;
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-27 wenzelm 2016-04-27 tuned;
2016-04-26 wenzelm 2016-04-26 merged
2016-04-26 wenzelm 2016-04-26 updated subtle side-conditions;
2016-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
2016-04-26 wenzelm 2016-04-26 'obtain' supports structured statements (similar to 'define');
2016-04-26 wenzelm 2016-04-26 more portable: GNU find no longer supports "-perm +mode";
2016-04-26 wenzelm 2016-04-26 more uniform operations for structured statements;
2016-04-26 wenzelm 2016-04-26 defs are closed, which leads to proper auto_bind_facts; misc tuning;
2016-04-26 wenzelm 2016-04-26 tuned notation;
2016-04-26 wenzelm 2016-04-26 misc tuning and modernization;
2016-04-22 hoelzl 2016-04-22 Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
2016-04-22 hoelzl 2016-04-22 Linear_Algebra: generalize linear_independent_extend to all real vector spaces
2016-04-22 hoelzl 2016-04-22 Linear_Algebra: alternative representation of linear combination