equal
deleted
inserted
replaced
6 begin |
6 begin |
7 |
7 |
8 notation (latex output) |
8 notation (latex output) |
9 Cons ("_ # _" [66,65] 65) |
9 Cons ("_ # _" [66,65] 65) |
10 |
10 |
11 (* rebinding of writeln and tracing so that it can *) |
|
12 (* be compared in intiquotations *) |
|
13 ML {* |
|
14 fun writeln s = (Output.writeln s; s) |
|
15 fun tracing s = (Output.tracing s; s) |
|
16 *} |
|
17 |
11 |
18 (* re-definition of various ML antiquotations *) |
12 (* re-definition of various ML antiquotations *) |
19 (* to have a special tag for text enclosed in ML; *) |
13 (* to have a special tag for text enclosed in ML; *) |
20 (* they also write the code into a separate file *) |
14 (* they also write the code into a separate file *) |
21 |
15 |