| 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 |