src/ZF/ex/BT.thy
changeset 1401 0c439768f45c
parent 1171 e4d6b42be73a
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/ex/BT.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/ex/BT.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,12 +8,12 @@
     1.4  
     1.5  BT = Datatype +
     1.6  consts
     1.7 -    bt_rec    	:: "[i, i, [i,i,i,i,i]=>i] => i"
     1.8 -    n_nodes	:: "i=>i"
     1.9 -    n_leaves   	:: "i=>i"
    1.10 -    bt_reflect 	:: "i=>i"
    1.11 +    bt_rec    	:: [i, i, [i,i,i,i,i]=>i] => i
    1.12 +    n_nodes	:: i=>i
    1.13 +    n_leaves   	:: i=>i
    1.14 +    bt_reflect 	:: i=>i
    1.15  
    1.16 -    bt 	        :: "i=>i"
    1.17 +    bt 	        :: i=>i
    1.18  
    1.19  datatype
    1.20    "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")