changeset 55075 | b3d0a02a756d |
parent 55071 | 8ae6f86a3477 |
child 57207 | df0f8ad7cc30 |
55074:2b0b6f69b148 | 55075:b3d0a02a756d |
---|---|
1 (* Title: HOL/BNF/Examples/TreeFI.thy |
1 (* Title: HOL/BNF_Examples/TreeFI.thy |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
3 Author: Andrei Popescu, TU Muenchen |
3 Author: Andrei Popescu, TU Muenchen |
4 Copyright 2012 |
4 Copyright 2012 |
5 |
5 |
6 Finitely branching possibly infinite trees. |
6 Finitely branching possibly infinite trees. |