src/HOL/Real/RealVector.thy
2007-04-10 huffman 2007-04-10 interpretation bounded_linear_of_real
2007-03-14 huffman 2007-03-14 move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
2006-12-13 huffman 2006-12-13 remove uses of scaleR infix syntax; add lemma Reals_number_of
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-10-02 huffman 2006-10-02 add lemmas norm_not_less_zero, norm_le_zero_iff
2006-09-28 wenzelm 2006-09-28 tuned definitions/proofs;
2006-09-28 huffman 2006-09-28 rearranged axioms and simp rules for scaleR
2006-09-27 huffman 2006-09-27 add lemmas about of_real and power
2006-09-27 huffman 2006-09-27 add lemmas of_int_in_Reals, of_nat_in_Reals
2006-09-24 huffman 2006-09-24 real_norm_def [simp]
2006-09-22 huffman 2006-09-22 add lemma norm_power
2006-09-19 huffman 2006-09-19 added classes real_div_algebra and real_field; added lemmas
2006-09-17 huffman 2006-09-17 norm_one is now proved from other class axioms
2006-09-16 huffman 2006-09-16 define new constant of_real for class real_algebra_1; define set Reals as range of_real; add lemmas about of_real and Reals
2006-09-16 huffman 2006-09-16 add theorem norm_diff_triangle_ineq
2006-09-14 huffman 2006-09-14 remove conflicting norm syntax
2006-09-12 huffman 2006-09-12 formalization of vector spaces and algebras over the real numbers