changeset 11316 | b4e71bd751e4 |
parent 6112 | 5e4871c5136b |
child 11354 | 9b80fe19407f |
--- a/src/ZF/ex/TF.thy Mon May 21 14:35:54 2001 +0200 +++ b/src/ZF/ex/TF.thy Mon May 21 14:36:24 2001 +0200 @@ -11,9 +11,9 @@ tree, forest, tree_forest :: i=>i datatype - "tree(A)" = Tcons ("a: A", "f: forest(A)") + "tree(A)" = Tcons ("a \\<in> A", "f \\<in> forest(A)") and - "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") + "forest(A)" = Fnil | Fcons ("t \\<in> tree(A)", "f \\<in> forest(A)") consts