Tuned.
authorberghofe
Tue, 27 Sep 2005 11:02:16 +0200
changeset 17662 c6165cf72e6a
parent 17661 994d010c0abd
child 17663 28be54ff74f8
Tuned.
doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Mon Sep 26 20:52:36 2005 +0200
+++ b/doc-src/HOL/HOL.tex	Tue Sep 27 11:02:16 2005 +0200
@@ -2811,7 +2811,7 @@
 
 The code generator is invoked via the \ttindex{code_module} and
 \ttindex{code_library} commands (see Fig.~\ref{fig:HOL:codegen-invocation}),
-which correspond to {\em modular} and {\em incremental} code generation,
+which correspond to {\em incremental} and {\em modular} code generation,
 respectively.
 \begin{description}
 \item[Modular] For each theory, an ML structure is generated, containing the