src/HOL/Library/Inner_Product.thy
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-03-17 hoelzl 2014-03-17 unify syntax for has_derivative and differentiable
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-26 huffman 2013-09-26 moved lemma
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-01-31 hoelzl 2013-01-31 remove unnecessary assumption from real_normed_vector
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
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