equal
deleted
inserted
replaced
1049 text {* |
1049 text {* |
1050 (FIXME: explain a version of rule-tac) |
1050 (FIXME: explain a version of rule-tac) |
1051 *} |
1051 *} |
1052 |
1052 |
1053 (*<*) |
1053 (*<*) |
1054 |
1054 (* THIS IS AN OLD VERSION OF THE PARSING CHAPTER BY JEREMY DAWSON *) |
1055 chapter {* Parsing *} |
1055 chapter {* Parsing *} |
1056 |
1056 |
1057 text {* |
1057 text {* |
1058 |
1058 |
1059 Lots of Standard ML code is given in this document, for various reasons, |
1059 Lots of Standard ML code is given in this document, for various reasons, |