src/HOL/Library/Inner_Product.thy
2011-09-12 huffman 2011-09-12 move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-16 huffman 2011-08-16 add simp rules for isCont
2011-08-09 huffman 2011-08-09 avoid duplicate rewrite warnings
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
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