equal
deleted
inserted
replaced
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 = |
14 val banner = |
15 "HOLCF with sections axioms,ops,domain,generated and 8bit characters"; |
15 "HOLCF with sections axioms,ops,domain,generated and 8bit characters"; |
16 (* end 8bit 1 *) |
16 (* end 8bit 1 *) |
17 |
17 |
18 writeln banner; |
18 writeln banner; |
19 print_depth 1; |
19 print_depth 1; |
20 |
20 |