src/Doc/Codegen/Evaluation.thy
changeset 63670 8e0148e1f5f4
parent 63175 d191892b1c23
child 65041 2525e680f94f
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Aug 11 18:26:44 2016 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Fri Aug 12 11:53:47 2016 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4    For technical reasons it is sometimes necessary to separate
     1.5    generation and compilation of code which is supposed to be used in
     1.6    the system runtime.  For this @{command code_reflect} with an
     1.7 -  optional @{text "file"} argument can be used:
     1.8 +  optional \<^theory_text>\<open>file\<close> argument can be used:
     1.9  \<close>
    1.10  
    1.11  code_reflect %quote Rat