src/HOL/Real_Vector_Spaces.thy
2016-02-08 hoelzl 2016-02-08 add type class for topological monoids
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-01-11 paulson 2016-01-11 nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2016-01-04 eberlm 2016-01-04 Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-12-23 immler 2015-12-23 transfer rule for bounded_linear of blinfun
2015-12-22 immler 2015-12-22 theory for type of bounded linear functions; differentiation under the integral sign
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-07-27 paulson 2015-07-27 New material for Cauchy's integral theorem
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-05-28 paulson 2015-05-28 Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-04-29 paulson 2015-04-29 Tidying. Improved simplification for numerals, esp in exponents.
2015-04-12 paulson 2015-04-12 Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]
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-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-09 paulson 2015-03-09 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
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-28 haftmann 2014-06-28 fact consolidation
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-03 paulson 2014-04-03 removing simprule status for divide_minus_left and divide_minus_right
2014-04-02 hoelzl 2014-04-02 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
2014-03-18 hoelzl 2014-03-18 fix HOL-NSA; move lemmas
2014-02-24 paulson 2014-02-24 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-16 immler 2013-12-16 lemmas about divideR and scaleR
2013-12-16 immler 2013-12-16 introduced ordered real vector spaces
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-12 huffman 2013-09-12 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-06-15 haftmann 2013-06-15 pragmatic executability for instance real :: open
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space