src/HOL/Real/RealVector.thy
Tue, 08 May 2007 18:23:37 +0200 huffman add lemmas norm_number_of, norm_of_int, norm_of_nat
less more (0) -10 -1 tip