src/HOL/IsaMakefile
changeset 24472 943ef707396c
parent 24470 41c81e23c08d
child 24540 68dab042dea8
--- a/src/HOL/IsaMakefile	Wed Aug 29 11:10:59 2007 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 29 13:58:00 2007 +0200
@@ -369,7 +369,7 @@
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
 
 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \
-  Hoare/Examples.thy Hoare/Hoare.thy \
+  Hoare/Examples.thy Hoare/Hoare.thy Hoare/hoare_tac.ML \
   Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
   Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \
   Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \
@@ -687,7 +687,7 @@
   Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
   Isar_examples/ROOT.ML Isar_examples/document/proof.sty \
   Isar_examples/document/root.bib Isar_examples/document/root.tex \
-  Isar_examples/document/style.tex Hoare/hoare.ML
+  Isar_examples/document/style.tex Hoare/hoare_tac.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples