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 +