--- a/src/HOL/ex/BT.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/BT.thy Fri Jul 24 13:19:38 1998 +0200
@@ -19,31 +19,31 @@
inorder :: 'a bt => 'a list
postorder :: 'a bt => 'a list
-primrec n_nodes bt
+primrec
"n_nodes (Lf) = 0"
"n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
-primrec n_leaves bt
+primrec
"n_leaves (Lf) = Suc 0"
"n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-primrec reflect bt
+primrec
"reflect (Lf) = Lf"
"reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-primrec bt_map bt
+primrec
"bt_map f Lf = Lf"
"bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
-primrec preorder bt
+primrec
"preorder (Lf) = []"
"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
-primrec inorder bt
+primrec
"inorder (Lf) = []"
"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
-primrec postorder bt
+primrec
"postorder (Lf) = []"
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"