src/HOL/Makefile
changeset 953 17d7fad9c9a2
parent 944 01d6571fa106
child 1044 5bf29088250e
     1.1 --- a/src/HOL/Makefile	Tue Mar 14 10:40:04 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Wed Mar 15 10:34:47 1995 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4  	case "$(COMP)" in \
     1.5  	poly*)	echo 'make_database"$(BIN)/CHOL"; quit();'  \
     1.6  			| $(COMP) $(BIN)/Pure;\
     1.7 -		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/CHOL ;;\
     1.8 -	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/CHOL" banner;' | $(BIN)/Pure ;;\
     1.9 +		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CHOL ;;\
    1.10 +	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/CHOL" banner;' | $(BIN)/Pure ;;\
    1.11  	*)	echo Bad value for ISABELLECOMP: \
    1.12                  	$(COMP) is not poly or sml; exit 1;;\
    1.13  	esac
    1.14 @@ -63,7 +63,7 @@
    1.15  IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
    1.16  
    1.17  IMP:    $(BIN)/CHOL  $(IMP_FILES)
    1.18 -	echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC)
    1.19 +	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
    1.20  
    1.21  ##The integers in CHOL
    1.22  INTEG_THYS = Integ/Relation.thy Integ/Equiv.thy Integ/Integ.thy 
    1.23 @@ -71,7 +71,7 @@
    1.24  INTEG_FILES = Integ/ROOT.ML $(INTEG_THYS) $(INTEG_THYS:.thy=.ML)
    1.25  
    1.26  Integ:  $(BIN)/CHOL  $(INTEG_FILES)
    1.27 -	echo 'use"Integ/ROOT.ML";quit();' | $(LOGIC)
    1.28 +	echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
    1.29  
    1.30  ##I/O Automata
    1.31  IOA_THYS = IOA/example/Action.thy IOA/example/Channels.thy\
    1.32 @@ -85,7 +85,7 @@
    1.33  	    $(IOA_THYS) $(IOA_THYS:.thy=.ML)
    1.34  
    1.35  IOA:    $(BIN)/CHOL  $(IOA_FILES)
    1.36 -	echo 'use"IOA/ROOT.ML";quit();' | $(LOGIC)
    1.37 +	echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC)
    1.38  
    1.39  ##Properties of substitutions
    1.40  SUBST_THYS = Subst/AList.thy Subst/Setplus.thy\
    1.41 @@ -95,7 +95,7 @@
    1.42  SUBST_FILES = Subst/ROOT.ML $(SUBST_THYS) $(SUBST_THYS:.thy=.ML)
    1.43  
    1.44  Subst:  $(BIN)/CHOL  $(SUBST_FILES)
    1.45 -	echo 'use"Subst/ROOT.ML";quit();' | $(LOGIC)
    1.46 +	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
    1.47  
    1.48  ##Miscellaneous examples
    1.49  EX_THYS = ex/LexProd.thy ex/MT.thy ex/Acc.thy \
    1.50 @@ -106,7 +106,7 @@
    1.51             ex/set.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    1.52  
    1.53  ex:     $(BIN)/CHOL  $(EX_FILES)
    1.54 -	echo 'use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.55 +	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.56  
    1.57  #Full test.
    1.58  test:   $(BIN)/CHOL IMP Integ IOA Subst ex