# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322660110 0
# Node ID 2862dacb04aa39cc41a6d9ea8bca0a23bc89f1f2
# Parent  1d1165432c9f50d32ac38dfbd05d198e6594d872
updated to Isabelle 30 November

diff -r 1d1165432c9f -r 2862dacb04aa ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri Nov 25 00:27:05 2011 +0000
+++ b/ProgTutorial/Essential.thy	Wed Nov 30 13:35:10 2011 +0000
@@ -2587,7 +2587,7 @@
   @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
   contains pretty-printing functions for terms, types, theorems and so on.
   
-  @{ML_file "Pure/General/markup.ML"}
+  @{ML_file "Pure/PIDE/markup.ML"}
   \end{readmore}
 *}
 
diff -r 1d1165432c9f -r 2862dacb04aa progtutorial.pdf
Binary file progtutorial.pdf has changed