# HG changeset patch
# User nipkow
# Date 816595521 -3600
# Node ID 38d66830a046e69ea7fa6f78030cf976dc8da055
# Parent  5e1c0540f2859297d997ea0ccf7be16052ba2542
Added Hoare.

diff -r 5e1c0540f285 -r 38d66830a046 src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Nov 17 09:04:10 1995 +0100
+++ b/src/HOL/Makefile	Fri Nov 17 09:05:21 1995 +0100
@@ -74,6 +74,13 @@
 IMP:    $(BIN)/HOL  $(IMP_FILES)
 	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
 
+##Hoare logic
+Hoare_NAMES = Hoare Arith2 Examples
+Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
+
+Hoare:  $(BIN)/HOL  $(Hoare_FILES)
+	echo 'exit_use"Hoare/ROOT.ML";quit();' | $(LOGIC)
+
 ##The integers in HOL
 INTEG_NAMES = Equiv Integ 
 
@@ -138,7 +145,7 @@
 	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
 
 #Full test. (IOA has been removed temporarily)
-test:   $(BIN)/HOL IMP Integ Subst Lambda MiniML IOA ex
+test:   $(BIN)/HOL IMP Hoare Integ Subst Lambda MiniML IOA ex
 	echo 'Test examples ran successfully' > test
 
 .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL