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