changeset 2278 | d63ffafce255 |
parent 2275 | dbce3dce821a |
child 2282 | 90fb68d597f8 |
2277:9174de6c7143 | 2278:d63ffafce255 |
---|---|
9 |
9 |
10 val banner = "HOLCF with sections axioms,ops,domain,generated"; |
10 val banner = "HOLCF with sections axioms,ops,domain,generated"; |
11 init_thy_reader(); |
11 init_thy_reader(); |
12 |
12 |
13 (* start 8bit 1 *) |
13 (* start 8bit 1 *) |
14 val banner = |
|
15 "HOLCF with sections axioms,ops,domain,generated and 8bit characters"; |
|
14 (* end 8bit 1 *) |
16 (* end 8bit 1 *) |
15 |
17 |
16 writeln banner; |
18 writeln banner; |
17 print_depth 1; |
19 print_depth 1; |
18 |
20 |