--- a/src/HOL/ex/BT.thy Tue Jul 30 18:03:11 1996 +0200
+++ b/src/HOL/ex/BT.thy Tue Jul 30 18:05:22 1996 +0200
@@ -20,31 +20,32 @@
postorder :: 'a bt => 'a list
primrec n_nodes bt
- n_nodes_Lf "n_nodes (Lf) = 0"
- n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
+ "n_nodes (Lf) = 0"
+ "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
primrec n_leaves bt
- n_leaves_Lf "n_leaves (Lf) = Suc 0"
- n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
+ "n_leaves (Lf) = Suc 0"
+ "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
primrec reflect bt
- reflect_Lf "reflect (Lf) = Lf"
- reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
+ "reflect (Lf) = Lf"
+ "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
primrec bt_map bt
- bt_map_Lf "bt_map f Lf = Lf"
- bt_map_Br "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+ "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
- preorder_Lf "preorder (Lf) = []"
- preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+ "preorder (Lf) = []"
+ "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
primrec inorder bt
- inorder_Lf "inorder (Lf) = []"
- inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+ "inorder (Lf) = []"
+ "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
primrec postorder bt
- postorder_Lf "postorder (Lf) = []"
- postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+ "postorder (Lf) = []"
+ "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
end
+