| changeset 256 | 1fb8d62c88a0 |
| parent 255 | ef1da1abee46 |
| child 260 | 5accec94b6df |
| 255:ef1da1abee46 | 256:1fb8d62c88a0 |
|---|---|
1 theory Base |
1 theory Base |
2 imports Main |
2 imports Main |
3 uses |
3 uses |
4 "outputfn.ML" |
4 "output_tutorial.ML" |
5 "chunks.ML" |
5 "chunks.ML" |
6 "antiquote_setup.ML" |
6 "antiquote_setup.ML" |
7 begin |
7 begin |
8 |
8 |
9 (* to have a special tag for text enclosed in ML *) |
9 (* to have a special tag for text enclosed in ML *) |