| changeset 12205 | f3545bd6669b |
| parent 12201 | 7198f403a2f9 |
| child 12216 | dda8c04a8fb4 |
--- 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)"}. *}