--- a/src/ZF/IsaMakefile Wed Jun 19 12:39:41 2002 +0200
+++ b/src/ZF/IsaMakefile Wed Jun 19 12:48:55 2002 +0200
@@ -10,7 +10,7 @@
images: ZF
#Note: keep targets sorted
-test: ZF-AC ZF-Coind ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
+test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
all: images test
@@ -73,6 +73,18 @@
@$(ISATOOL) usedir $(OUT)/ZF Coind
+## ZF-Constructible
+
+ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz
+
+$(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML \
+ Constructible/Formula.thy Constructible/Relative.thy \
+ Constructible/L_axioms.thy Constructible/Wellorderings.thy \
+ Constructible/Normal.thy Constructible/WF_absolute.thy \
+ Constructible/Reflection.thy Constructible/WFrec.thy
+ @$(ISATOOL) usedir $(OUT)/ZF Constructible
+
+
## ZF-IMP
ZF-IMP: ZF $(LOG)/ZF-IMP.gz
@@ -134,5 +146,6 @@
clean:
@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \
- $(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
+ $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \
+ $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
$(LOG)/ZF-UNITY.gz