src/HOL/RealVector.thy
2013-01-31 hoelzl 2013-01-31 introduce order topology
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-11 wenzelm 2012-03-11 eliminated old-fashioned 'constrains' element;
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-08-28 huffman 2011-08-28 move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-09 huffman 2011-08-09 lemma bounded_linear_intro
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
2010-08-20 haftmann 2010-08-20 more concise characterization of of_nat operation and class semiring_char_0
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-11 huffman 2010-05-11 no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-10 huffman 2010-05-10 new construction of real numbers using Cauchy sequences
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2009-06-12 huffman 2009-06-12 declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
2009-06-11 huffman 2009-06-11 new lemmas
2009-06-11 huffman 2009-06-11 theorem attribute [tendsto_intros]
2009-06-11 huffman 2009-06-11 subsection for real instances; new lemmas for open sets of reals
2009-06-07 huffman 2009-06-07 fix type of open
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-07 huffman 2009-06-07 move definitions of open, closed to RealVector.thy
2009-06-04 huffman 2009-06-04 add extra type constraints for dist, norm
2009-06-03 huffman 2009-06-03 more [code del] declarations
2009-06-03 huffman 2009-06-03 replace class open with class topo
2009-06-03 huffman 2009-06-03 introduce class topological_space as a superclass of metric_space
2009-05-28 huffman 2009-05-28 move dist operation to new metric_space class
2009-05-28 huffman 2009-05-28 generalize dist function to class real_normed_vector
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-22 huffman 2009-02-22 declare scaleR distrib rules [algebra_simps]; cleaned up
2009-02-22 huffman 2009-02-22 clean up instantiations
2009-01-21 haftmann 2009-01-21 no base sort in class import
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout