changeset 896 | 56b9c2626e81 |
parent 895 | 7a1e07fbffea |
child 897 | 55d15c603e3a |
895:7a1e07fbffea | 896:56b9c2626e81 |
---|---|
1 (* |
1 (* $Id$ *) |
2 ID: $Id$ |
|
3 *) |
|
4 |
|
5 |
2 |
6 open Dagstuhl; |
3 open Dagstuhl; |
7 |
4 |
8 val YS_def2 = fix_prover Dagstuhl.thy YS_def "YS = scons[y][YS]"; |
5 val YS_def2 = fix_prover Dagstuhl.thy YS_def "YS = scons[y][YS]"; |
9 val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]"; |
6 val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]"; |