tuned;
authorwenzelm
Fri Aug 12 11:53:47 2016 +0200 (2016-08-12)
changeset 636708e0148e1f5f4
parent 63669 256fc20716f2
child 63671 eb4f59275c05
tuned;
src/Doc/Codegen/Evaluation.thy
     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