--- a/src/ZF/Bin.thy Sun Jun 24 11:41:41 2018 +0100
+++ b/src/ZF/Bin.thy Sun Jun 24 15:57:48 2018 +0200
@@ -16,7 +16,7 @@
section\<open>Arithmetic on Binary Integers\<close>
theory Bin
-imports Int_ZF Datatype_ZF
+imports Int Datatype
begin
consts bin :: i