| Wed, 14 Mar 2007 21:40:28 +0100 | huffman | move bounded (bi)linear operator locales from Lim.thy to RealVector.thy | file | diff | annotate |
| Wed, 13 Dec 2006 00:02:53 +0100 | huffman | remove uses of scaleR infix syntax; add lemma Reals_number_of | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Tue, 07 Nov 2006 11:47:57 +0100 | wenzelm | renamed 'const_syntax' to 'notation'; | file | diff | annotate |
| Mon, 02 Oct 2006 18:30:10 +0200 | huffman | add lemmas norm_not_less_zero, norm_le_zero_iff | file | diff | annotate |
| Thu, 28 Sep 2006 23:42:47 +0200 | wenzelm | tuned definitions/proofs; | file | diff | annotate |
| Thu, 28 Sep 2006 19:04:13 +0200 | huffman | rearranged axioms and simp rules for scaleR | file | diff | annotate |