--- a/src/ZF/ex/TF.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/TF.thy Wed Jan 13 11:57:09 1999 +0100
@@ -8,6 +8,15 @@
TF = List +
consts
+ tree, forest, tree_forest :: i=>i
+
+datatype
+ "tree(A)" = Tcons ("a: A", "f: forest(A)")
+and
+ "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
+
+
+consts
map :: [i=>i, i] => i
size :: i=>i
preorder :: i=>i
@@ -15,13 +24,6 @@
of_list :: i=>i
reflect :: i=>i
- tree, forest, tree_forest :: i=>i
-
-datatype
- "tree(A)" = Tcons ("a: A", "f: forest(A)")
-and
- "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
-
primrec
"list_of_TF (Tcons(x,f)) = [Tcons(x,f)]"
"list_of_TF (Fnil) = []"