author | Christian Urban <urbanc@in.tum.de> |
Mon, 17 Oct 2011 13:30:49 +0100 | |
changeset 473 | fea1b7ce5c4a |
parent 472 | 1bbe4268664d |
child 474 | 683fb6e468b1 |
child 475 | 25371f74c768 |
ProgTutorial/Parsing.thy | file | annotate | diff | comparison | revisions | |
progtutorial.pdf | file | annotate | diff | comparison | revisions |
--- 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: