# HG changeset patch
# User berghofe
# Date 1127811736 -7200
# Node ID c6165cf72e6a9f1cd70e3348fa59d6d113bfa62e
# Parent  994d010c0abda184623c5d37aff1fe2a90234e72
Tuned.

diff -r 994d010c0abd -r c6165cf72e6a 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