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
2013-04-25 hoelzl 2013-04-25 renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-26 hoelzl 2013-03-26 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26 hoelzl 2013-03-26 rename RealVector.thy to Real_Vector_Spaces.thy