# HG changeset patch
# User oheimb
# Date 962981162 -7200
# Node ID 5f39d82606aad5c096d6c51049d96c9ea103911c
# Parent  21c302a2fd9a6c21ddd5aeefff014ac0a023e9ee
added IMP/Examples.ML dependence

diff -r 21c302a2fd9a -r 5f39d82606aa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jul 06 18:12:17 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri Jul 07 16:46:02 2000 +0200
@@ -151,8 +151,8 @@
 
 $(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/Examples.thy IMP/ROOT.ML IMP/Transition.ML\
-  IMP/Transition.thy IMP/VC.ML IMP/VC.thy
+  IMP/Natural.ML IMP/Natural.thy IMP/Examples.ML IMP/Examples.thy \
+  IMP/Transition.ML IMP/Transition.thy IMP/VC.ML IMP/VC.thy IMP/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL IMP