src/HOL/Integ/IntDef.thy
Fri, 27 Aug 1999 15:42:10 +0200 paulson tidied, allowing pattern-matching in defs of zadd and zmult
less more (0) -1 tip