| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 30 Nov 2011 13:35:10 +0000 | |
| changeset 505 | 2862dacb04aa |
| parent 504 | 1d1165432c9f |
| child 506 | caa733190454 |
| child 507 | d770a7b31aeb |
| ProgTutorial/Essential.thy | file | annotate | diff | comparison | revisions | |
| progtutorial.pdf | file | annotate | diff | comparison | revisions |
--- 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} *}