src/ZF/ex/BT.thy
changeset 1171 e4d6b42be73a
parent 935 a94ef3eed456
child 1401 0c439768f45c
equal deleted inserted replaced
1170:39119c4c7bac 1171:e4d6b42be73a
     1 (*  Title: 	ZF/ex/bt-fn.thy
     1 (*  Title: 	ZF/ex/BT.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Binary trees
     6 Binary trees