# HG changeset patch
# User paulson
# Date 1026204281 -7200
# Node ID 3f475e54875c62255e423933b9a97f07c60bbe1e
# Parent  bb74918cc0dd9cc34b88fccfe2ea476973840dc4
new files

diff -r bb74918cc0dd -r 3f475e54875c src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Mon Jul 08 18:49:18 2002 +0200
+++ b/src/ZF/IsaMakefile	Tue Jul 09 10:44:41 2002 +0200
@@ -78,9 +78,11 @@
 ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz
 
 $(LOG)/ZF-Constructible.gz: $(OUT)/ZF  Constructible/ROOT.ML \
+  Constructible/Datatype_absolute.thy\
   Constructible/Formula.thy     Constructible/Relative.thy \
   Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
-  Constructible/Normal.thy      Constructible/WF_absolute.thy \
+  Constructible/MetaExists.thy  Constructible/Normal.thy \
+  Constructible/Separation.thy      Constructible/WF_absolute.thy \
   Constructible/Reflection.thy  Constructible/WFrec.thy \
   Constructible/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/ZF Constructible