| changeset 15131 | c69542757a4d |
| parent 15047 | fa62de5862b9 |
| child 15140 | 322485b816ac |
--- a/src/HOL/Integ/IntDef.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Integ/IntDef.thy Mon Aug 16 14:22:27 2004 +0200 @@ -7,7 +7,9 @@ header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} -theory IntDef = Equiv + NatArith: +theory IntDef +import Equiv NatArith +begin constdefs intrel :: "((nat * nat) * (nat * nat)) set"