# HG changeset patch
# User lcp
# Date 777288316 -7200
# Node ID 93dc86ccee288a97998bbb65b4d9bcceded225ae
# Parent  5b96b1252cdc4879b93bf0b3f40cefe05636c459
HOL/Makefile, ROOT: updated for new .thy files

diff -r 5b96b1252cdc -r 93dc86ccee28 Makefile
--- a/Makefile	Fri Aug 19 11:19:14 1994 +0200
+++ b/Makefile	Fri Aug 19 11:25:16 1994 +0200
@@ -19,9 +19,10 @@
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
 FILES = ROOT.ML HOL.thy HOL.ML simpdata.ML Ord.thy Ord.ML \
-	fun.ML Set.thy Set.ML subset.ML equalities.ML \
+	Set.thy Set.ML Fun.thy Fun.ML subset.thy subset.ML \
+	equalities.thy equalities.ML \
 	Prod.thy Prod.ML Sum.thy Sum.ML WF.thy WF.ML \
-	mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
+	mono.thy mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
         Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
         LList.thy LList.ML List.thy List.ML \
 	Datatype.ML \
diff -r 5b96b1252cdc -r 93dc86ccee28 ROOT.ML
--- a/ROOT.ML	Fri Aug 19 11:19:14 1994 +0200
+++ b/ROOT.ML	Fri Aug 19 11:25:16 1994 +0200
@@ -77,13 +77,10 @@
 
 use     "simpdata.ML";
 use_thy "Ord";
-use_thy "Set";
-use     "fun.ML";
-use     "subset.ML";
-use     "equalities.ML";
+use_thy "subset";
+use_thy "equalities";
 use_thy "Prod";
 use_thy "Sum";
-use     "mono.ML";
 use_thy "LList";
 
 use "../Pure/install_pp.ML";