# 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.