changeset 61670 | 301e0b4ecd45 |
parent 61566 | c3d6e570ccef |
child 61671 | 20d4cd2ceab2 |
--- 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 \<open> 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 \<close> (*<*)