isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

src/HOL/Real/RealVector.thy

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

less more (0) tip

isabelle

RSS Atom