src/HOL/Real/RealVector.thy
Wed, 06 Jun 2007 20:49:04 +0200 huffman add axclass semiring_char_0 for types where of_nat is injective
less more (0) -30 -10 -1 tip