src/HOL/Real/RealVector.thy
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-08-27 huffman 2008-08-27 simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
2008-08-26 huffman 2008-08-26 move real_vector class proofs into vector_space and group_hom locales
2008-07-11 huffman 2008-07-11 instance real_field < field_char_0; instance star :: (field_char_0) field_char_0
2008-07-11 haftmann 2008-07-11 re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
2008-07-10 huffman 2008-07-10 instance real_field < field_char_0
2008-07-02 huffman 2008-07-02 use begin and end for proofs in locales
2008-07-02 haftmann 2008-07-02 cleaned up some code generator configuration
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-08 haftmann 2007-10-08 added first version of user-space type system for class target
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-15 haftmann 2007-09-15 introduced classes
2007-09-02 huffman 2007-09-02 fix sgn_div_norm class
2007-09-01 wenzelm 2007-09-01 removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;
2007-09-01 nipkow 2007-09-01 final(?) iteration of sgn saga.
2007-06-06 huffman 2007-06-06 add axclass semiring_char_0 for types where of_nat is injective
2007-05-30 huffman 2007-05-30 simplify names of locale interpretations
2007-05-29 huffman 2007-05-29 interpretation bounded_linear_divide
2007-05-28 huffman 2007-05-28 interpretations additive_scaleR_left, additive_scaleR_right
2007-05-14 huffman 2007-05-14 add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
2007-05-14 huffman 2007-05-14 generalized sgn function to work on any real normed vector space
2007-05-12 huffman 2007-05-12 add lemma additive.setsum
2007-05-10 huffman 2007-05-10 instance real_algebra_1 < ring_char_0
2007-05-09 huffman 2007-05-09 add lemma norm_diff_ineq; shorten other proofs
2007-05-09 huffman 2007-05-09 add lemmas norm_add_less, norm_mult_less
2007-05-08 huffman 2007-05-08 add lemmas norm_number_of, norm_of_int, norm_of_nat
2007-05-08 huffman 2007-05-08 add lemma abs_norm_cancel
2007-05-07 huffman 2007-05-07 clean up RealVector classes
2007-04-11 huffman 2007-04-11 new class syntax for scaleR and norm classes
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