changeset 473 | fea1b7ce5c4a |
parent 472 | 1bbe4268664d |
child 514 | 7e25716c3744 |
--- a/ProgTutorial/Parsing.thy Sun Jul 31 00:00:58 2011 +0100 +++ b/ProgTutorial/Parsing.thy Mon Oct 17 13:30:49 2011 +0100 @@ -783,7 +783,7 @@ \begin{readmore} The functions to do with input and output of XML and YXML are defined - in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}. + in @{ML_file "Pure/PIDE/xml.ML"} and @{ML_file "Pure/PIDE/yxml.ML"}. \end{readmore} FIXME: