# HG changeset patch
# User wenzelm
# Date 1005844577 -3600
# Node ID f3545bd6669bfbbba6f717d12e320112c77263f9
# Parent  98115606ee426da7c9d5b93b7b7e1646b366d383
fixed;

diff -r 98115606ee42 -r f3545bd6669b src/ZF/Induct/ROOT.ML
--- a/src/ZF/Induct/ROOT.ML	Thu Nov 15 18:15:58 2001 +0100
+++ b/src/ZF/Induct/ROOT.ML	Thu Nov 15 18:16:17 2001 +0100
@@ -9,7 +9,7 @@
 time_use_thy "Datatypes";
 time_use_thy "Binary_Trees";
 time_use_thy "Term";            (*recursion over the list functor*)
-time_use_thy "Tree_Forest"      (*mutual recursion*)
+time_use_thy "Tree_Forest";     (*mutual recursion*)
 time_use_thy "Mutil";           (*mutilated chess board*)
 
 (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
diff -r 98115606ee42 -r f3545bd6669b src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Thu Nov 15 18:15:58 2001 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Thu Nov 15 18:16:17 2001 +0100
@@ -28,7 +28,7 @@
 
 
 text {*
-  \medskip @{term "tree_forest(A)" as the union of @{term "tree(A)"}
+  \medskip @{term "tree_forest(A)"} as the union of @{term "tree(A)"}
   and @{term "forest(A)"}.
 *}