Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added Hoare.
authornipkow
Fri, 17 Nov 1995 09:05:21 +0100
changeset 1336 38d66830a046
parent 1335 5e1c0540f285
child 1337 ad834f39d878
Added Hoare.
src/HOL/Makefile file | annotate | diff | comparison | revisions 
--- 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
isabelle