--- a/src/ZF/Makefile Fri Oct 22 13:42:51 1993 +0100
+++ b/src/ZF/Makefile Fri Oct 22 13:43:45 1993 +0100
@@ -32,7 +32,7 @@
$(BIN)/ZF: $(BIN)/FOL $(FILES)
case "$(COMP)" in \
poly*) cp $(BIN)/FOL $(BIN)/ZF;\
- echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
+ echo 'open PolyML; use"ROOT";' | $(COMP) -h 15000 $(BIN)/ZF ;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
*) echo Bad value for ISABELLECOMP;;\
esac
@@ -42,7 +42,7 @@
test: ex/ROOT.ML $(BIN)/ZF
case "$(COMP)" in \
- poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
+ poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) -h 15000 $(BIN)/ZF ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\
*) echo Bad value for ISABELLECOMP;;\
esac
--- a/src/ZF/ROOT.ML Fri Oct 22 13:42:51 1993 +0100
+++ b/src/ZF/ROOT.ML Fri Oct 22 13:43:45 1993 +0100
@@ -11,6 +11,8 @@
val banner = "ZF Set Theory (in FOL)";
writeln banner;
+set_loadpath [".", "ex", "../FOL"];
+
(*For Pure/tactic?? A crude way of adding structure to rules*)
fun CHECK_SOLVED (Tactic tf) =
Tactic (fn state =>
@@ -66,7 +68,7 @@
use "datatype.ML";
use "fin.ML";
-use "list.ML";
+use_thy "List";
use_thy "listfn";
(*printing functions are inherited from FOL*)