--- 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 \
--- 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";