--- a/src/HOL/IsaMakefile Wed Jul 05 17:42:06 2000 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 05 17:52:24 2000 +0200
@@ -151,7 +151,7 @@
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Denotation.ML \
IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
- IMP/Natural.ML IMP/Natural.thy IMP/Example.thy IMP/ROOT.ML IMP/Transition.ML \
+ IMP/Natural.ML IMP/Natural.thy IMP/Examples.thy IMP/ROOT.ML IMP/Transition.ML\
IMP/Transition.thy IMP/VC.ML IMP/VC.thy
@$(ISATOOL) usedir $(OUT)/HOL IMP