Now calls exit_use instead of use, for prompt failure if errors are detected.
--- a/src/ZF/Makefile Wed Mar 15 10:56:39 1995 +0100
+++ b/src/ZF/Makefile Wed Mar 15 10:59:20 1995 +0100
@@ -35,8 +35,8 @@
$(BIN)/ZF: $(BIN)/FOL $(FILES)
case "$(COMP)" in \
poly*) cp $(BIN)/FOL $(BIN)/ZF;\
- echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
- sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
+ echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
+ sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml; exit 1;;\
esac
@@ -59,7 +59,7 @@
IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
IMP: $(BIN)/ZF $(IMP_FILES)
- echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC)
+ echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
##Coinduction example
COIND_THYS = Coind/ECR.thy Coind/Language.thy\
@@ -70,7 +70,7 @@
$(COIND_THYS) $(COIND_THYS:.thy=.ML)
Coind: $(BIN)/ZF $(COIND_FILES)
- echo 'use"Coind/ROOT.ML";quit();' | $(LOGIC)
+ echo 'exit_use"Coind/ROOT.ML";quit();' | $(LOGIC)
##Miscellaneous examples
EX_THYS = ex/Ramsey.thy ex/Integ.thy ex/twos_compl.thy ex/Bin.thy \
@@ -82,7 +82,7 @@
#Test ZF by loading the examples in directory ex
ex: $(BIN)/ZF $(EX_FILES)
- echo 'use"ex/ROOT.ML";quit();' | $(LOGIC)
+ echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
#Full test.
test: $(BIN)/ZF IMP Coind ex