changeset 3953 | 473ea5ce5ca8 |
parent 3623 | e843c1d6f9e1 |
child 4008 | 2444085532c6 |
3952:dca1bce88ec8 | 3953:473ea5ce5ca8 |
---|---|
7 Should be executed in subdirectory HOLCF. |
7 Should be executed in subdirectory HOLCF. |
8 *) |
8 *) |
9 |
9 |
10 val banner = "HOLCF"; |
10 val banner = "HOLCF"; |
11 writeln banner; |
11 writeln banner; |
12 |
|
13 set global_names; |
|
12 |
14 |
13 print_depth 1; |
15 print_depth 1; |
14 |
16 |
15 use_thy "HOLCF"; |
17 use_thy "HOLCF"; |
16 |
18 |