src/HOL/Multivariate_Analysis/Operator_Norm.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-03-28 huffman 2014-03-28 minimized imports
2014-03-19 huffman 2014-03-19 generalize theory of operator norms to work with class real_normed_vector
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-09-18 wenzelm 2013-09-18 tuned proofs;
2013-08-28 wenzelm 2013-08-28 tuned proofs;
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2011-08-10 huffman 2011-08-10 split Linear_Algebra.thy from Euclidean_Space.thy
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-04-29 huffman 2010-04-29 define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-28 huffman 2010-04-28 move operator norm stuff to new theory file