# HG changeset patch
# User wenzelm
# Date 864387119 -7200
# Node ID b00902bb16caf94a9ae8209af030ef5b1a55a3e0
# Parent  6ec687d436aa15b6a14cec114884b89217ba53b7
removed TFL from test;

diff -r 6ec687d436aa -r b00902bb16ca src/HOL/Makefile
--- a/src/HOL/Makefile	Fri May 23 11:28:22 1997 +0200
+++ b/src/HOL/Makefile	Fri May 23 13:31:59 1997 +0200
@@ -77,17 +77,6 @@
 			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
 	esac`
 
-##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:	$(BIN)/HOL  $(TFL_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html:= true; exit_use_dir"../TFL";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"../TFL";quit();' | $(LOGIC); \
-	fi
-
 
 ## Inductive definitions: simple examples
 
@@ -229,7 +218,7 @@
 
 #Full test.
 test:	$(BIN)/HOL \
-		TFL Induct IMP Hoare Lex Integ Auth Subst Lambda  \
+		Induct IMP Hoare Lex Integ Auth Subst Lambda  \
 		W0 MiniML IOA AxClasses Quot ex
 	echo 'Test examples ran successfully' > test