--- a/src/ZF/ex/TF.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/TF.thy Sat Dec 09 13:36:11 1995 +0100
@@ -8,14 +8,14 @@
TF = List +
consts
- TF_rec :: "[i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i"
- TF_map :: "[i=>i, i] => i"
- TF_size :: "i=>i"
- TF_preorder :: "i=>i"
- list_of_TF :: "i=>i"
- TF_of_list :: "i=>i"
+ TF_rec :: [i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i
+ TF_map :: [i=>i, i] => i
+ TF_size :: i=>i
+ TF_preorder :: i=>i
+ list_of_TF :: i=>i
+ TF_of_list :: i=>i
- tree, forest, tree_forest :: "i=>i"
+ tree, forest, tree_forest :: i=>i
datatype
"tree(A)" = Tcons ("a: A", "f: forest(A)")