src/HOL/Integ/Bin.thy

--- a/src/HOL/Integ/Bin.thy	Fri Sep 18 16:04:44 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Fri Sep 18 16:05:08 1998 +0200
@@ -86,11 +86,6 @@
 	            (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" 
 
 
-(*For implementing the equality test on integer constants*)
-constdefs
-  iszero :: int => bool
-  "iszero z == z = $# 0"
-  
 end
 
 ML