changeset 1171 | e4d6b42be73a |
parent 935 | a94ef3eed456 |
child 1401 | 0c439768f45c |
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 |