src/HOL/IntDef.thy
Sat, 09 Jun 2007 02:38:51 +0200 huffman remove dependencies of proofs on constant int::nat=>int, preparing to remove it
Wed, 06 Jun 2007 20:49:04 +0200 huffman add axclass semiring_char_0 for types where of_nat is injective
less more (0) -2 tip