# HG changeset patch
# User haftmann
# Date 1644648754 -3600
# Node ID 78c2a92a8be405385c6a419c5a2bb6579cef286c
# Parent  f8008b40b8a0aef9683d9758cdf8c5879b4a1ea4
updated documentation to current matter of affairs

diff -r f8008b40b8a0 -r 78c2a92a8be4 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Thu Feb 10 19:38:12 2022 +0100
+++ b/src/Doc/Codegen/Further.thy	Sat Feb 12 07:52:34 2022 +0100
@@ -40,7 +40,7 @@
   For technical reasons it is sometimes necessary to separate
   generation and compilation of code which is supposed to be used in
   the system runtime.  For this @{command code_reflect} with an
-  optional \<^theory_text>\<open>file\<close> argument can be used:
+  optional \<^theory_text>\<open>file_prefix\<close> argument can be used:
 \<close>
 
 code_reflect %quote Rat
@@ -51,8 +51,8 @@
   file_prefix rat
 
 text \<open>
-  \noindent This merely generates the referenced code to the given
-  file which can be included into the system runtime later on.
+  \noindent This generates the referenced code as logical files within the theory context,
+  similar to @{command export_code}.
 \<close>
 
 subsection \<open>Specialities of the \<open>Scala\<close> target language \label{sec:scala}\<close>