# HG changeset patch
# User nipkow
# Date 801583810 -7200
# Node ID 866fff8576267ba6eabe3469ea7d62f34cb33cd4
# Parent  64b30e3cc6d4721c86fb3b4d3d6ec84cbb28d03a
Moved Relation from Integ to main HOL.

diff -r 64b30e3cc6d4 -r 866fff857626 src/HOL/Makefile
--- a/src/HOL/Makefile	Fri May 26 18:11:47 1995 +0200
+++ b/src/HOL/Makefile	Sat May 27 16:10:10 1995 +0200
@@ -18,7 +18,7 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-NAMES = HOL Ord Set Fun subset equalities Prod Trancl Sum WF \
+NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
        mono Lfp Gfp Nat Inductive Finite Arith Sexp Univ List 
 
 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
@@ -64,7 +64,7 @@
 	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
 
 ##The integers in CHOL
-INTEG_NAMES = Relation Equiv Integ 
+INTEG_NAMES = Equiv Integ 
 
 INTEG_FILES = Integ/ROOT.ML \
               $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)