src/ZF/Integ/Bin.thy
changeset 11381 4ab3b7b0938f
parent 9570 e16e168984e1
child 12182 3f820a21dcc1
--- a/src/ZF/Integ/Bin.thy	Tue Jun 26 16:54:39 2001 +0200
+++ b/src/ZF/Integ/Bin.thy	Tue Jun 26 17:04:09 2001 +0200
@@ -14,8 +14,6 @@
 
 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
-
-Division is not defined yet!
 *)
 
 Bin = Int + Datatype +