equal
deleted
inserted
replaced
224 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
224 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
225 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
225 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
226 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
226 \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} |
227 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
227 \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} |
228 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
228 \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} |
|
229 \item @{text phi} for morphisms; ML-type @{ML_type morphism} |
229 \end{itemize} |
230 \end{itemize} |
230 *} |
231 *} |
231 |
232 |
232 section {* Acknowledgements *} |
233 section {* Acknowledgements *} |
233 |
234 |