# HG changeset patch
# User nipkow
# Date 1021024545 -7200
# Node ID bb448fb7519182316348100adbc3979b0ab64dd5
# Parent  99f6a9f0328adb7ab09704ea51dd10dd10bfb2a0
added dep on IMP/Compiler0

diff -r 99f6a9f0328a -r bb448fb75191 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 10 10:22:45 2002 +0200
+++ b/src/HOL/IsaMakefile	Fri May 10 11:55:45 2002 +0200
@@ -233,7 +233,7 @@
 
 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
 
-$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler.thy \
+$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy IMP/Compiler.thy \
   IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
   IMP/Natural.thy IMP/Examples.thy \
   IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \