2016-10-01 wenzelm 2016-10-01 Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-10-01 wenzelm 2016-10-01 clarified lfp/gfp statements and proofs;
2016-10-01 Lars Hupel 2016-10-01 repair LaTeX
2016-10-01 wenzelm 2016-10-01 misc tuning for release;
2016-10-01 wenzelm 2016-10-01 added lemma;
2016-09-30 paulson 2016-09-30 Trying out "subgoal", and no more [| |]
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: fix latex generation
2016-09-30 hoelzl 2016-09-30 Probability: fix proof
2016-09-30 hoelzl 2016-09-30 Library: fix name Product_plus to Product_Plus
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Product_Vector and Inner_Product from Library
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Continuum_Not_Denumerable from Library
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-30 paulson 2016-09-30 new material on paths, etc. Also rationalisation
2016-09-30 Manuel Eberl 2016-09-30 Merged
2016-09-29 eberlm 2016-09-29 Set_Permutations replaced by more general Multiset_Permutations
2016-09-29 boehmes 2016-09-29 CONTRIBUTORS: new proof method "argo"
2016-09-29 boehmes 2016-09-29 NEWS: new proof method "argo"
2016-09-29 boehmes 2016-09-29 use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
2016-09-29 boehmes 2016-09-29 invoke argo as part of the tried automatic proof methods
2016-09-29 boehmes 2016-09-29 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: move gauges and (tagged) divisions to its own theory file
2016-09-28 hoelzl 2016-09-28 HOL-Analysis: add cover lemma ported by L. C. Paulson
2016-09-29 paulson 2016-09-29 more new material
2016-09-29 paulson 2016-09-29 Generalised the type of map_poly
2016-09-28 paulson 2016-09-28 Merge
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-09-28 Lars Hupel 2016-09-28 sequential (jobs = 1) makeall profile
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-09-26 haftmann 2016-09-26 dropped tautological pattern
2016-09-26 haftmann 2016-09-26 more warning comments
2016-09-26 haftmann 2016-09-26 more lemmas
2016-09-26 haftmann 2016-09-26 spelling
2016-09-27 paulson 2016-09-27 a few new theorems and a renaming
2016-09-26 hoelzl 2016-09-26 use filter to define Henstock-Kurzweil integration
2016-09-24 Lars Hupel 2016-09-24 include generation time in statistics
2016-09-24 Lars Hupel 2016-09-24 CI script to generate timing statistics
2016-09-23 hoelzl 2016-09-23 move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
2016-09-23 hoelzl 2016-09-23 prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
2016-09-22 paulson 2016-09-22 Merge
2016-09-22 paulson 2016-09-22 More mainly topological results
2016-09-22 wenzelm 2016-09-22 merged
2016-09-22 wenzelm 2016-09-22 discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;
2016-09-22 wenzelm 2016-09-22 raw control symbols are superseded by Latex.embed_raw;
2016-09-21 wenzelm 2016-09-21 \<^raw> output is intended for LaTeX;
2016-09-21 wenzelm 2016-09-21 more general mixfix delimiters;
2016-09-21 wenzelm 2016-09-21 more tight implementation of symbol explode operation (without support for raw symbols);
2016-09-21 immler 2016-09-21 approximation: preprocessing for nat/int expressions
2016-09-21 immler 2016-09-21 provide more information on error
2016-09-21 immler 2016-09-21 approximation: rewrite for reduction to base expressions
2016-09-21 paulson 2016-09-21 new material about topological concepts, etc
2016-09-21 paulson 2016-09-21 vector_add_divide_simps now a "named theorems" bundle
2016-09-20 wenzelm 2016-09-20 tuned -- fewer warnings;
2016-09-20 wenzelm 2016-09-20 avoid old SML90;
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-09-20 eberlm 2016-09-20 NEWS: Normalized_Fraction.thy
2016-09-20 eberlm 2016-09-20 Merged
2016-09-19 eberlm 2016-09-19 Additions to permutations (contributed by Lukas Bulwahn)