diff -r 1757a6e049f4 -r a63501938ce1 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Fri Mar 28 00:02:54 2008 +0100
+++ b/src/HOLCF/IsaMakefile	Fri Mar 28 00:02:56 2008 +0100
@@ -27,15 +27,16 @@
 HOL:
 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
 
-$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.thy Cont.thy Cprod.thy			\
-  Discrete.thy Domain.thy Ffun.thy Fix.thy Fixrec.thy HOLCF.thy Lift.thy	\
-  One.thy Pcpo.thy Pcpodef.thy Porder.thy ROOT.ML Sprod.thy Ssum.thy		\
-  Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML			\
-  Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML			\
-  Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML			\
-  Tools/domain/domain_theorems.ML Tools/fixrec_package.ML			\
-  Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex	\
-  holcf_logic.ML
+$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Bifinite.thy Cfun.thy			\
+  CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy		\
+  Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy		\
+  LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy SetPcpo.thy	\
+  Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML			\
+  Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML		\
+  Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML		\
+  Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML		\
+  Tools/domain/domain_theorems.ML Tools/fixrec_package.ML		\
+  Tools/pcpodef_package.ML document/root.tex holcf_logic.ML
 	@$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF