equal
deleted
inserted
replaced
139 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
139 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
140 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
140 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
141 \end{itemize} |
141 \end{itemize} |
142 *} |
142 *} |
143 |
143 |
|
144 section {* Aaaaargh! My Code Does not Work Anymore (TBD) *} |
|
145 |
|
146 text {* |
|
147 |
|
148 *} |
|
149 |
144 section {* Acknowledgements *} |
150 section {* Acknowledgements *} |
145 |
151 |
146 text {* |
152 text {* |
147 Financial support for this tutorial was provided by the German |
153 Financial support for this tutorial was provided by the German |
148 Research Council (DFG) under grant number URB 165/5-1. The following |
154 Research Council (DFG) under grant number URB 165/5-1. The following |