--- a/src/HOLCF/IsaMakefile Tue Jul 01 06:56:37 2008 +0200
+++ b/src/HOLCF/IsaMakefile Tue Jul 01 07:13:45 2008 +0200
@@ -27,17 +27,50 @@
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
-$(OUT)/HOLCF: $(OUT)/HOL Adm.thy Algebraic.thy Bifinite.thy Cfun.thy \
- CompactBasis.thy Completion.thy Cont.thy ConvexPD.thy Cprod.thy \
- Discrete.thy Deflation.thy Domain.thy Eventual.thy Ffun.thy \
- Fixrec.thy Fix.thy HOLCF.thy Lift.thy LowerPD.thy NatIso.thy \
- One.thy Pcpodef.thy Pcpo.thy Porder.thy Sprod.thy Ssum.thy Tr.thy \
- Universal.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
+$(OUT)/HOLCF: $(OUT)/HOL \
+ ROOT.ML \
+ Adm.thy \
+ Algebraic.thy \
+ Bifinite.thy \
+ Cfun.thy \
+ CompactBasis.thy \
+ Completion.thy \
+ Cont.thy \
+ ConvexPD.thy \
+ Cprod.thy \
+ Discrete.thy \
+ Deflation.thy \
+ Domain.thy \
+ Eventual.thy \
+ Ffun.thy \
+ Fixrec.thy \
+ Fix.thy \
+ HOLCF.thy \
+ Lift.thy \
+ LowerPD.thy \
+ NatIso.thy \
+ One.thy \
+ Pcpodef.thy \
+ Pcpo.thy \
+ Porder.thy \
+ Sprod.thy \
+ Ssum.thy \
+ Tr.thy \
+ Universal.thy \
+ UpperPD.thy \
+ Up.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 \
+ holcf_logic.ML \
+ document/root.tex
@$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF