Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
authorwenzelm
Thu, 15 Nov 2001 18:20:13 +0100
changeset 12207 4dff931b852f
parent 12206 60d52181840c
child 12208 5efe7b6874fd
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
src/ZF/IsaMakefile file | annotate | diff | comparison | revisions 
--- 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
isabelle