# HG changeset patch
# User wenzelm
# Date 1005776165 -3600
# Node ID 9b7026a0b0ed5b959c1dbaa3561d2d099ddf5368
# Parent  54bd9aa3343d41b030acc015e6bb21da093a1668
added Induct/Binary_Trees.thy, Induct/Datatypes.thy;
removed ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy;

diff -r 54bd9aa3343d -r 9b7026a0b0ed src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed Nov 14 23:15:19 2001 +0100
+++ b/src/ZF/IsaMakefile	Wed Nov 14 23:16:05 2001 +0100
@@ -125,12 +125,13 @@
 ZF-Induct: ZF $(LOG)/ZF-Induct.gz
 
 $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
-  Induct/Comb.ML Induct/Comb.thy  Induct/FoldSet.ML Induct/FoldSet.thy \
-  Induct/ListN.ML Induct/ListN.thy \
+  Induct/Binary_Trees.thy Induct/Comb.ML Induct/Comb.thy Induct/Datatypes.thy \
+  Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML Induct/ListN.thy \
   Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
   Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
   Induct/Primrec.ML Induct/Primrec.thy \
-  Induct/PropLog.ML Induct/PropLog.thy  Induct/Rmap.ML Induct/Rmap.thy
+  Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy \
+  Induct/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/ZF Induct
 
 
@@ -138,10 +139,9 @@
 
 ZF-ex: ZF $(LOG)/ZF-ex.gz
 
-$(LOG)/ZF-ex.gz: $(OUT)/ZF  ex/ROOT.ML ex/BT.ML ex/BT.thy \
+$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
   ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
   ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
-  ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \
   ex/Limit.ML ex/Limit.thy  ex/LList.ML ex/LList.thy\
   ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy\
   ex/NatSum.ML ex/NatSum.thy \