added dependencies on ax_ops/*.ML and domain/*.ML
authoroheimb
Thu, 24 Apr 1997 10:40:01 +0200
changeset 3028 45204c79ad1d
parent 3027 ce99919010bf
child 3029 db0e9b30dc92
added dependencies on ax_ops/*.ML and domain/*.ML
src/HOLCF/IsaMakefile
src/HOLCF/Makefile
--- a/src/HOLCF/IsaMakefile	Thu Apr 24 10:39:00 1997 +0200
+++ b/src/HOLCF/IsaMakefile	Thu Apr 24 10:40:01 1997 +0200
@@ -17,11 +17,15 @@
        Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
        One.thy Tr.thy\
        Discrete0.thy Discrete1.thy Discrete.thy\
-       Lift1.thy Lift2.thy Lift3.thy HOLCF.thy 
+       Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
 
 ONLYTHYS = Lift.thy
 
-FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
+FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
+        ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \ 
+        ax_ops/thy_ops.ML    ax_ops/thy_syntax.ML \
+        domain/library.ML  domain/syntax.ML   domain/axioms.ML \
+        domain/theorems.ML domain/extender.ML domain/interface.ML
 
 $(OUT)/HOLCF: $(OUT)/HOL $(FILES)
 	@$(ISATOOL) usedir -b -c $(OUT)/HOL HOLCF
--- a/src/HOLCF/Makefile	Thu Apr 24 10:39:00 1997 +0200
+++ b/src/HOLCF/Makefile	Thu Apr 24 10:40:01 1997 +0200
@@ -33,7 +33,11 @@
 
 ONLYTHYS = Lift.thy
 
-FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
+FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
+        ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \ 
+        ax_ops/thy_ops.ML    ax_ops/thy_syntax.ML \
+        domain/library.ML  domain/syntax.ML   domain/axioms.ML \
+        domain/theorems.ML domain/extender.ML domain/interface.ML
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/HOLCF:	$(BIN)/HOL  $(FILES)