# 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)