src/ZF/IsaMakefile
changeset 12207 4dff931b852f
parent 12186 9b7026a0b0ed
child 12229 bfba0eb5124b
--- a/src/ZF/IsaMakefile	Thu Nov 15 18:18:17 2001 +0100
+++ b/src/ZF/IsaMakefile	Thu Nov 15 18:20:13 2001 +0100
@@ -131,7 +131,7 @@
   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/document/root.tex
+  Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/ZF Induct
 
 
@@ -142,11 +142,9 @@
 $(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/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 \
-  ex/Ramsey.ML ex/Ramsey.thy  ex/TF.ML ex/TF.thy \
-  ex/Term.ML ex/Term.thy ex/misc.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 ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
 	@$(ISATOOL) usedir $(OUT)/ZF ex