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