changeset 229 | abc7f90188af |
parent 228 | fe45fbb111c5 |
child 230 | 8def50824320 |
--- a/ProgTutorial/Parsing.thy Fri Apr 03 07:55:07 2009 +0100 +++ b/ProgTutorial/Parsing.thy Tue Apr 07 17:04:39 2009 +0100 @@ -748,6 +748,11 @@ \end{exercise} *} +text {* + (FIXME: @{ML OuterParse.type_args}, @{ML OuterParse.typ}, @{ML OuterParse.opt_mixfix}) +*} + + section {* New Commands and Keyword Files\label{sec:newcommand} *} text {*