# HG changeset patch
# User wenzelm
# Date 1327494716 -3600
# Node ID e18ccb00fb8ff41e003da55298b8b65b4e565fce
# Parent  3e427a12f0f3f4b384af9e1e7f9d92f14feb406e
tuned;

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}
diff -r 3e427a12f0f3 -r e18ccb00fb8f doc-src/IsarImplementation/Thy/document/Logic.tex
--- 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}