diff -r 27ca6147e3b3 -r 301e0b4ecd45 src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:51 2015 +0100 +++ b/src/Doc/Codegen/Further.thy Sat Nov 14 08:45:52 2015 +0100 @@ -220,8 +220,7 @@ (*>*) text \ Fortunately, an even more succint approach is available using command - @{command permanent_interpretation}. This is available - by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}. + @{command permanent_interpretation}. Then the pattern above collapses to \ (*<*)