src/HOL/Library/Inner_Product.thy
2009-06-12 huffman 2009-06-12 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-04 huffman 2009-06-04 add extra type constraints for dist, norm
2009-06-03 huffman 2009-06-03 replace class open with class topo
2009-06-03 huffman 2009-06-03 class real_inner derives from open_dist
2009-05-28 huffman 2009-05-28 move dist operation to new metric_space class
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-22 huffman 2009-02-22 simplify some proofs
2009-02-21 huffman 2009-02-21 fix spelling
2009-02-19 huffman 2009-02-19 new theory of real inner product spaces