# 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 \