--- a/src/HOL/ex/BT.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/BT.thy Fri Dec 01 12:03:13 1995 +0100
@@ -11,13 +11,13 @@
datatype 'a bt = Lf | Br 'a ('a bt) ('a bt)
consts
- n_nodes :: "'a bt => nat"
- n_leaves :: "'a bt => nat"
- reflect :: "'a bt => 'a bt"
- bt_map :: "('a=>'b) => ('a bt => 'b bt)"
- preorder :: "'a bt => 'a list"
- inorder :: "'a bt => 'a list"
- postorder :: "'a bt => 'a list"
+ n_nodes :: 'a bt => nat
+ n_leaves :: 'a bt => nat
+ reflect :: 'a bt => 'a bt
+ bt_map :: ('a=>'b) => ('a bt => 'b bt)
+ preorder :: 'a bt => 'a list
+ inorder :: 'a bt => 'a list
+ postorder :: 'a bt => 'a list
primrec n_nodes bt
n_nodes_Lf "n_nodes (Lf) = 0"