# HG changeset patch
# User nipkow
# Date 808756721 -7200
# Node ID 56ee5cc3551004d7bee73cac4324e8db5942a0fb
# Parent  2856f382f033a028e49568714cc15f756dacd0f7
updated "o" in HOL: (infixl 55)
added warning about conj_cong in HOL.

diff -r 2856f382f033 -r 56ee5cc35510 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Aug 18 16:09:41 1995 +0200
+++ b/doc-src/Logics/HOL.tex	Fri Aug 18 16:38:41 1995 +0200
@@ -78,7 +78,7 @@
 \begin{tabular}{rrrr} 
   \it symbol    & \it meta-type & \it priority & \it description \\ 
   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
-        Right 50 & composition ($\circ$) \\
+        Left 55 & composition ($\circ$) \\
   \tt =         & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
   \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
   \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 & 
@@ -922,10 +922,18 @@
 simplification set for higher-order logic.  Equality~($=$), which also
 expresses logical equivalence, may be used for rewriting.  See the file
 {\tt HOL/simpdata.ML} for a complete listing of the simplification
-rules. 
+rules.
 \item 
 It instantiates the classical reasoner, as described below. 
 \end{itemize}
+\begin{warn}\index{simplification!of conjunctions}
+  The simplifier is not set up to reduce, for example, \verb$a = b & ...a...$
+  to \verb$a = b & ...b...$: it does not use the left part of a conjunction
+  while simplifying the right part. This can be changed by including
+  \ttindex{conj_cong} in a simpset: \verb$addcongs [conj_cong]$. It can slow
+  down rewriting and is therefore not included by default.
+\end{warn}
+
 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
 rule; recall Fig.\ts\ref{hol-lemmas2} above.