src/HOL/ex/BT.thy
changeset 1376 92f83b9d17e1
parent 1167 cbd32a0f2f41
child 1476 608483c2122a
--- 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"