# HG changeset patch
# User paulson
# Date 863693619 -7200
# Node ID dcb458d38724801287b35b8ea5f1e1b4381a7f66
# Parent  36bfceef18006663758a9eb2c5306388f9a566b0
Preliminary TFL versions

diff -r 36bfceef1800 -r dcb458d38724 src/HOL/IsaMakefile
--- 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
 
diff -r 36bfceef1800 -r dcb458d38724 src/HOL/ROOT.ML
--- 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;