added -h 15000 for Poly/ML in Makefile,
authorclasohm
Fri Oct 22 13:43:45 1993 +0100 (1993-10-22)
changeset 75144ec40f2650
parent 74 208ab8773a73
child 76 c616d66c640e
added -h 15000 for Poly/ML in Makefile,
changed ROOT.ML for new Readthy
src/ZF/Makefile
src/ZF/ROOT.ML
     1.1 --- a/src/ZF/Makefile	Fri Oct 22 13:42:51 1993 +0100
     1.2 +++ b/src/ZF/Makefile	Fri Oct 22 13:43:45 1993 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
     1.5  	case "$(COMP)" in \
     1.6  	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
     1.7 -		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
     1.8 +		echo 'open PolyML; use"ROOT";' | $(COMP) -h 15000 $(BIN)/ZF ;;\
     1.9  	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
    1.10  	*)	echo Bad value for ISABELLECOMP;;\
    1.11  	esac
    1.12 @@ -42,7 +42,7 @@
    1.13  
    1.14  test:   ex/ROOT.ML  $(BIN)/ZF
    1.15  	case "$(COMP)" in \
    1.16 -	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
    1.17 +	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) -h 15000 $(BIN)/ZF ;;\
    1.18  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\
    1.19  	*)	echo Bad value for ISABELLECOMP;;\
    1.20  	esac
     2.1 --- a/src/ZF/ROOT.ML	Fri Oct 22 13:42:51 1993 +0100
     2.2 +++ b/src/ZF/ROOT.ML	Fri Oct 22 13:43:45 1993 +0100
     2.3 @@ -11,6 +11,8 @@
     2.4  val banner = "ZF Set Theory (in FOL)";
     2.5  writeln banner;
     2.6  
     2.7 +set_loadpath [".", "ex", "../FOL"];
     2.8 +
     2.9  (*For Pure/tactic??  A crude way of adding structure to rules*)
    2.10  fun CHECK_SOLVED (Tactic tf) = 
    2.11    Tactic (fn state => 
    2.12 @@ -66,7 +68,7 @@
    2.13  use     "datatype.ML";
    2.14  
    2.15  use     "fin.ML";
    2.16 -use     "list.ML";
    2.17 +use_thy "List";
    2.18  use_thy "listfn";
    2.19  
    2.20  (*printing functions are inherited from FOL*)