src/HOL/Real/RealVector.thy
Wed, 02 Jul 2008 19:35:43 +0200 huffman use begin and end for proofs in locales
less more (0) -30 -10 -1 tip