| author | haftmann |
| Fri, 17 Mar 2006 14:20:24 +0100 | |
| changeset 19281 | b411f25fff25 |
| parent 17291 | 94f6113fe9ed |
| child 19742 | 86f21beabafc |
| permissions | -rw-r--r-- |
| 2570 | 1 |
(* $Id$ *) |
2 |
||
| 17291 | 3 |
theory Dagstuhl |
4 |
imports Stream |
|
5 |
begin |
|
| 2570 | 6 |
|
7 |
consts |
|
| 17291 | 8 |
y :: "'a" |
| 2570 | 9 |
|
| 17291 | 10 |
constdefs |
11 |
YS :: "'a stream" |
|
12 |
"YS == fix$(LAM x. y && x)" |
|
13 |
YYS :: "'a stream" |
|
14 |
"YYS == fix$(LAM z. y && y && z)" |
|
| 2570 | 15 |
|
| 17291 | 16 |
ML {* use_legacy_bindings (the_context ()) *}
|
17 |
||
| 2570 | 18 |
end |
19 |