2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-03-16 paulson 2017-03-16 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
2017-01-04 paulson 2017-01-04 Many new theorems, and more tidying
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 paulson 2016-09-30 new material on paths, etc. Also rationalisation
2016-09-22 wenzelm 2016-09-22 raw control symbols are superseded by Latex.embed_raw;
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-09-15 paulson 2016-09-15 simple new lemmas, mostly about sets
2016-08-25 Manuel Eberl 2016-08-25 More analysis lemmas
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-09 haftmann 2016-07-09 more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
2016-07-02 haftmann 2016-07-02 more theorems
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-27 wenzelm 2016-05-27 tuned proofs;
2016-05-23 paulson 2016-05-23 Lots of new material for multivariate analysis
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-01 wenzelm 2016-04-01 explicit property for unbreakable block;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-09 hoelzl 2016-02-09 instantiate topologies for nat, int and enat
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-11 eberlm 2016-01-11 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-21 paulson 2015-09-21 new lemmas and movement of lemmas into place
2015-07-28 paulson 2015-07-28 the Cauchy integral theorem and related material
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-30 paulson 2015-06-30 Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-06-26 wenzelm 2015-06-26 proper spacing, as for other syntax for these symbols;
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-01-20 hoelzl 2015-01-20 generalized sum_diff_distrib to setsum_subtractf_nat
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-11 noschinl 2014-11-11 add forgotten lemma
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-05-29 paulson 2014-05-29 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
2014-05-13 hoelzl 2014-05-13 clean up Lebesgue integration
2014-04-09 hoelzl 2014-04-09 field_simps: better support for negation and division, and power
2014-03-31 hoelzl 2014-03-31 add rules about infinity of intervals
2014-03-21 paulson 2014-03-21 a few new lemmas and generalisations of old ones
2014-03-19 paulson 2014-03-19 New complex analysis material
2014-03-18 hoelzl 2014-03-18 fix HOL-NSA; move lemmas
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-02-24 paulson 2014-02-24 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
2014-02-24 paulson 2014-02-24 A few lemmas about summations, etc.
2014-02-02 paulson 2014-02-02 Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.