# HG changeset patch
# User paulson
# Date 1024483735 -7200
# Node ID b6fc6e4a0a24296a304a07dde707a3a823612d83
# Parent  6f0928a942d152c71fd2cafad4302cfd82f3a25c
added the Constructible target

diff -r 6f0928a942d1 -r b6fc6e4a0a24 src/ZF/IsaMakefile
--- 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