src/ZF/ex/Bin.thy
changeset 589 31847a7504ec
parent 515 abcc438e7c27
child 753 ec86863e87c8
--- a/src/ZF/ex/Bin.thy	Wed Sep 07 13:04:28 1994 +0200
+++ b/src/ZF/ex/Bin.thy	Wed Sep 07 17:28:53 1994 +0200
@@ -6,7 +6,7 @@
 Arithmetic on binary integers.
 *)
 
-Bin = Integ + Univ + 
+Bin = Integ + Univ + "twos_compl" +
 consts
   bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
   integ_of_bin     :: "i=>i"