--- a/src/HOL/IsaMakefile Thu May 15 12:53:12 1997 +0200
+++ b/src/HOL/IsaMakefile Thu May 15 12:53:39 1997 +0200
@@ -8,9 +8,9 @@
OUT = $(ISABELLE_OUTPUT)
-NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
+NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
- Sexp Univ List RelPow Option
+ Psubset Sexp Univ List RelPow Option
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
ind_syntax.ML cladata.ML simpdata.ML \
@@ -28,17 +28,6 @@
@cd ../Pure; $(ISATOOL) make
-## TFL (requires integration into HOL proper)
-
-TFL_NAMES = mask tfl thms thry usyntax utils
-TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
- $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
-
-TFL: $(OUT)/HOL $(TFL_FILES)
- @$(ISABELLE) -qe 'exit_use_dir"../TFL"; quit();' HOL
-
-
-
#### Tests and examples
## Inductive definitions: simple examples
@@ -105,7 +94,7 @@
## Properties of substitutions
-SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
+SUBST_NAMES = AList Subst Unifier UTerm Unify
SUBST_FILES = Subst/ROOT.ML \
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
@@ -208,7 +197,7 @@
## Full test
test: $(OUT)/HOL \
- TFL Induct IMP Hoare Lex Integ Auth Subst Lambda \
+ Subst Induct IMP Hoare Lex Integ Auth Lambda \
W0 MiniML IOA AxClasses Quot ex
echo 'Test examples ran successfully' > test
--- a/src/HOL/ROOT.ML Thu May 15 12:53:12 1997 +0200
+++ b/src/HOL/ROOT.ML Thu May 15 12:53:39 1997 +0200
@@ -41,8 +41,14 @@
use_thy "Finite";
use_thy "Sexp";
use_thy "Option";
+use_thy "WF_Rel";
use_thy "List";
+(*TFL: recursive function definitions*)
+cd "../TFL";
+use "sys.sml";
+cd "../HOL";
+
init_pps ();
print_depth 8;