src/HOL/Makefile
changeset 1336 38d66830a046
parent 1329 8987c0df4b2f
child 1343 8770c062b092
     1.1 --- a/src/HOL/Makefile	Fri Nov 17 09:04:10 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Fri Nov 17 09:05:21 1995 +0100
     1.3 @@ -74,6 +74,13 @@
     1.4  IMP:    $(BIN)/HOL  $(IMP_FILES)
     1.5  	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
     1.6  
     1.7 +##Hoare logic
     1.8 +Hoare_NAMES = Hoare Arith2 Examples
     1.9 +Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
    1.10 +
    1.11 +Hoare:  $(BIN)/HOL  $(Hoare_FILES)
    1.12 +	echo 'exit_use"Hoare/ROOT.ML";quit();' | $(LOGIC)
    1.13 +
    1.14  ##The integers in HOL
    1.15  INTEG_NAMES = Equiv Integ 
    1.16  
    1.17 @@ -138,7 +145,7 @@
    1.18  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.19  
    1.20  #Full test. (IOA has been removed temporarily)
    1.21 -test:   $(BIN)/HOL IMP Integ Subst Lambda MiniML IOA ex
    1.22 +test:   $(BIN)/HOL IMP Hoare Integ Subst Lambda MiniML IOA ex
    1.23  	echo 'Test examples ran successfully' > test
    1.24  
    1.25  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL