--- 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