--- 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}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 13:24:57 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 13:31:56 2012 +0100
@@ -943,14 +943,16 @@
%
\endisadelimmlantiq
%
-\isamarkupsubsection{Auxiliary definitions \label{sec:logic-aux}%
+\isamarkupsubsection{Auxiliary connectives \label{sec:logic-aux}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Theory \isa{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.
+Theory \isa{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}