src/HOL/Real_Vector_Spaces.thy
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