# HG changeset patch
# User paulson
# Date 901875128 -7200
# Node ID 092e77b6f7c6d47350c264a7a68beea355d48e8d
# Parent  8d132a14e722ff94804cf2c61e97690afe8a66aa
Removed HOL/IMP/Com.ML because it contained only an "open" declaration

diff -r 8d132a14e722 -r 092e77b6f7c6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jul 31 10:50:47 1998 +0200
+++ b/src/HOL/IsaMakefile	Fri Jul 31 10:52:08 1998 +0200
@@ -88,7 +88,7 @@
 
 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
 
-$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
+$(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/ROOT.ML IMP/Transition.ML \
   IMP/Transition.thy IMP/VC.ML IMP/VC.thy