src/HOL/Library/Inner_Product.thy
2009-02-21 huffman 2009-02-21 fix spelling
2009-02-19 huffman 2009-02-19 new theory of real inner product spaces