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