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