# HG changeset patch
# User lcp
# Date 778951733 -7200
# Node ID 31847a7504ecbde8de2d9e29de4be6c364838088
# Parent  91d5ac5ebb1739ebeeb3ca95d47652eadf53f1a3
addition of ZF/ex/twos_compl.thy

diff -r 91d5ac5ebb17 -r 31847a7504ec src/ZF/Makefile
--- 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 \
diff -r 91d5ac5ebb17 -r 31847a7504ec src/ZF/ex/Bin.thy
--- 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"
diff -r 91d5ac5ebb17 -r 31847a7504ec src/ZF/ex/ROOT.ML
--- 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 **)
diff -r 91d5ac5ebb17 -r 31847a7504ec src/ZF/ex/twos_compl.thy
--- /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