# HG changeset patch
# User wenzelm
# Date 899390679 -7200
# Node ID 2497807020fa0b84837c0e143a5e18d25bfc9989
# Parent  b3d18eb3ac204fc81c8860a29650c80b70e7be2c
fixed Integ;

diff -r b3d18eb3ac20 -r 2497807020fa src/HOL/Integ/ROOT.ML
--- a/src/HOL/Integ/ROOT.ML	Wed Jul 01 19:11:20 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*  Title:      HOL/Integ/ROOT
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-
-The Integers in HOL (ported from ZF by Riccardo Mattolini)
-*)
-
-time_use_thy "Bin";
diff -r b3d18eb3ac20 -r 2497807020fa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 01 19:11:20 1998 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 02 16:44:39 1998 +0200
@@ -39,22 +39,19 @@
   $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
   $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
   $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
-  Integ/Bin.ML Integ/Bin.thy  Integ/Equiv.ML Integ/Equiv.thy \
-  Integ/Integ.ML Integ/Integ.thy Integ/ROOT.ML \
-  Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \
-  Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
-  Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
+  Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
+  Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
+  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
+  Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
-  Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
+  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Record.thy RelPow.ML \
   RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
-  Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \
-  Tools/inductive_package.ML \
-  Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML \
-  WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML cladata.ML \
-  datatype.ML equalities.ML equalities.thy hologic.ML \
-  mono.ML mono.thy \
-  simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML
+  Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
+  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
+  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
+  WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
+  equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
+  subset.thy thy_data.ML thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
@@ -342,7 +339,7 @@
 clean:
 	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
 	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
-	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
+	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
 	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
 	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
 	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
diff -r b3d18eb3ac20 -r 2497807020fa src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Jul 01 19:11:20 1998 +0200
+++ b/src/HOL/ROOT.ML	Thu Jul 02 16:44:39 1998 +0200
@@ -57,7 +57,7 @@
 use_thy "Update";
 
 cd "Integ";
-use "ROOT.ML";
+use_thy "Bin";
 cd "..";
 
 (*TFL: recursive function definitions*)