src/ZF/ex/BT.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
     1.1 --- a/src/ZF/ex/BT.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/ex/BT.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/ex/BT.thy
     1.5 +(*  Title:      ZF/ex/BT.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11  Binary trees
    1.12 @@ -8,12 +8,12 @@
    1.13  
    1.14  BT = Datatype +
    1.15  consts
    1.16 -    bt_rec    	:: [i, i, [i,i,i,i,i]=>i] => i
    1.17 -    n_nodes	:: i=>i
    1.18 -    n_leaves   	:: i=>i
    1.19 -    bt_reflect 	:: i=>i
    1.20 +    bt_rec      :: [i, i, [i,i,i,i,i]=>i] => i
    1.21 +    n_nodes     :: i=>i
    1.22 +    n_leaves    :: i=>i
    1.23 +    bt_reflect  :: i=>i
    1.24  
    1.25 -    bt 	        :: i=>i
    1.26 +    bt          :: i=>i
    1.27  
    1.28  datatype
    1.29    "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
    1.30 @@ -22,8 +22,8 @@
    1.31    bt_rec_def
    1.32      "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
    1.33  
    1.34 -  n_nodes_def	"n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
    1.35 -  n_leaves_def	"n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
    1.36 +  n_nodes_def   "n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
    1.37 +  n_leaves_def  "n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
    1.38    bt_reflect_def "bt_reflect(t) == bt_rec(t,  Lf,  %x y z r s. Br(x,s,r))"
    1.39  
    1.40  end