# HG changeset patch
# User paulson
# Date 855914237 -3600
# Node ID 15451c558a32fbcf2a003305a9f7e733cb6d9fe4
# Parent  b94dadf5b6bebd11000a3309a140e0baf936024f
Deleted a useless definition

diff -r b94dadf5b6be -r 15451c558a32 src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Fri Feb 14 10:41:02 1997 +0100
+++ b/src/HOL/Integ/Integ.thy	Fri Feb 14 10:57:17 1997 +0100
@@ -19,9 +19,6 @@
 
 constdefs
 
-  zNat        :: nat set
-  "zNat == {x::nat. True}"
-
   znat        :: nat => int                                  ("$# _" [80] 80)
   "$# m == Abs_Integ(intrel ^^ {(m,0)})"