src/HOL/ex/BT.thy
changeset 1376 92f83b9d17e1
parent 1167 cbd32a0f2f41
child 1476 608483c2122a
     1.1 --- a/src/HOL/ex/BT.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/BT.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -11,13 +11,13 @@
     1.4  datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
     1.5    
     1.6  consts
     1.7 -    n_nodes	:: "'a bt => nat"
     1.8 -    n_leaves   	:: "'a bt => nat"
     1.9 -    reflect 	:: "'a bt => 'a bt"
    1.10 -    bt_map      :: "('a=>'b) => ('a bt => 'b bt)"
    1.11 -    preorder    :: "'a bt => 'a list"
    1.12 -    inorder     :: "'a bt => 'a list"
    1.13 -    postorder   :: "'a bt => 'a list"
    1.14 +    n_nodes	:: 'a bt => nat
    1.15 +    n_leaves   	:: 'a bt => nat
    1.16 +    reflect 	:: 'a bt => 'a bt
    1.17 +    bt_map      :: ('a=>'b) => ('a bt => 'b bt)
    1.18 +    preorder    :: 'a bt => 'a list
    1.19 +    inorder     :: 'a bt => 'a list
    1.20 +    postorder   :: 'a bt => 'a list
    1.21  
    1.22  primrec n_nodes bt
    1.23    n_nodes_Lf "n_nodes (Lf) = 0"