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