src/HOL/Real_Vector_Spaces.thy
20 months ago paulson 2017-10-09 new material about connectedness, etc.
22 months ago paulson 2017-08-14 patching the previous commit
22 months ago paulson 2017-08-14 further Hensock tidy-up
2017-06-15 paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
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-02-21 paulson 2017-02-21 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2017-01-05 paulson 2017-01-05 New material about path connectedness, etc.
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-16 haftmann 2016-10-16 more standardized names
2016-09-30 paulson 2016-09-30 new material on paths, etc. Also rationalisation
2016-09-21 paulson 2016-09-21 vector_add_divide_simps now a "named theorems" bundle
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-07-28 immler 2016-07-28 numerical bounds on pi
2016-07-22 wenzelm 2016-07-22 misc tuning and modernization;
2016-07-13 paulson 2016-07-13 lots of new theorems about differentiable_on, retracts, ANRs, etc.
2016-05-24 paulson 2016-05-24 renamings and new material
2016-05-23 paulson 2016-05-23 Lots of new material for multivariate analysis
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-11 paulson 2016-04-11 lots of new theorems for multivariate analysis
2016-03-15 paulson 2016-03-15 rationalisation of theorem names esp about "real Archimedian" etc.
2016-03-07 paulson 2016-03-07 new material to Blochj's theorem, as well as supporting lemmas
2016-02-24 paulson 2016-02-24 Substantial new material for multivariate analysis. Also removal of some duplicates.
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-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.