src/HOL/Real_Vector_Spaces.thy
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Wed, 02 Apr 2014 18:35:01 +0200 hoelzl moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Tue, 18 Mar 2014 16:29:32 +0100 hoelzl fix HOL-NSA; move lemmas
Mon, 24 Feb 2014 16:56:04 +0000 paulson Lemmas about Reals, norm, etc., and cleaner variants of existing ones
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Mon, 16 Dec 2013 17:08:22 +0100 immler lemmas about divideR and scaleR
Mon, 16 Dec 2013 17:08:22 +0100 immler introduced ordered real vector spaces
Mon, 09 Dec 2013 12:22:23 +0100 wenzelm more antiquotations;
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Tue, 05 Nov 2013 09:45:02 +0100 hoelzl move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Thu, 12 Sep 2013 18:09:17 -0700 huffman make 'linear' into a sublocale of 'bounded_linear';
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Sat, 15 Jun 2013 17:19:23 +0200 haftmann pragmatic executability for instance real :: open
Thu, 25 Apr 2013 11:59:21 +0200 hoelzl revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
Thu, 25 Apr 2013 10:35:56 +0200 hoelzl renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl 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
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Tue, 26 Mar 2013 12:21:01 +0100 hoelzl remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
Tue, 26 Mar 2013 12:20:57 +0100 hoelzl rename RealVector.thy to Real_Vector_Spaces.thy
less more (0) tip