--- a/src/ZF/Makefile Wed Sep 07 13:04:28 1994 +0200
+++ b/src/ZF/Makefile Wed Sep 07 17:28:53 1994 +0200
@@ -43,7 +43,7 @@
EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\
ex/Integ.ML ex/Integ.thy\
- ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\
+ ex/twos_compl.thy ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\
ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \
ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \
ex/Brouwer.thy ex/Brouwer.ML \
--- 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"
--- a/src/ZF/ex/ROOT.ML Wed Sep 07 13:04:28 1994 +0200
+++ b/src/ZF/ex/ROOT.ML Wed Sep 07 17:28:53 1994 +0200
@@ -17,8 +17,6 @@
time_use_thy "ex/Ramsey";
(*Integers & Binary integer arithmetic*)
-use "ex/twos_compl.ML"; (*can delete after autoloader change
- and addition of "twos_compl" to Bin.thy*)
time_use_thy "ex/Bin";
(** Datatypes **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/twos_compl.thy Wed Sep 07 17:28:53 1994 +0200
@@ -0,0 +1,8 @@
+(* ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+*)
+
+(*Dummy theory; allows twos_compl itself to be a dependency *)
+
+twos_compl = Pure