diff -r 3e427a12f0f3 -r e18ccb00fb8f doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Wed Jan 25 13:24:57 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Wed Jan 25 13:31:56 2012 +0100
@@ -830,12 +830,13 @@
 *}
 
 
-subsection {* Auxiliary definitions \label{sec:logic-aux} *}
+subsection {* Auxiliary connectives \label{sec:logic-aux} *}
 
-text {*
-  Theory @{text "Pure"} provides a few auxiliary definitions, see
-  \figref{fig:pure-aux}.  These special constants are normally not
-  exposed to the user, but appear in internal encodings.
+text {* Theory @{text "Pure"} provides a few auxiliary connectives
+  that are defined on top of the primitive ones, see
+  \figref{fig:pure-aux}.  These special constants are useful in
+  certain internal encodings, and are normally not directly exposed to
+  the user.
 
   \begin{figure}[htb]
   \begin{center}