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