# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1318854649 -3600
# Node ID fea1b7ce5c4a9d974300e2b111571ec188a059e8
# Parent  1bbe4268664d328ed119dec7ebac1cede7f3857a
this version works with Isabelle2011-1

diff -r 1bbe4268664d -r fea1b7ce5c4a ProgTutorial/Parsing.thy
--- 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:
diff -r 1bbe4268664d -r fea1b7ce5c4a progtutorial.pdf
Binary file progtutorial.pdf has changed