# HG changeset patch
# User nipkow
# Date 954335391 -7200
# Node ID c99e0024050c5cde004d4e8d37482a17be3f6b9f
# Parent  805910de7be0a08f069f08e25e3dfb16d890c7e9
*** empty log message ***

diff -r 805910de7be0 -r c99e0024050c doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Wed Mar 29 14:23:27 2000 +0200
+++ b/doc-src/HOL/HOL.tex	Wed Mar 29 15:09:51 2000 +0200
@@ -936,6 +936,14 @@
   including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
 \end{warn}
 
+\begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%
+  By default only the condition of an \ttindex{if} is simplified but not the
+  \texttt{then} and \texttt{else} parts. Of course the latter are simplified
+  once the condition simplifies to \texttt{True} or \texttt{False}. To ensure
+  full simplification of all parts of a conditional you must remove
+  \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.
+\end{warn}
+
 If the simplifier cannot use a certain rewrite rule --- either because
 of nontermination or because its left-hand side is too flexible ---
 then you might try \texttt{stac}:
@@ -2135,6 +2143,16 @@
 This theorem can be added to a simpset via \ttindex{addsplits}
 (see~{\S}\ref{subsec:HOL:case:splitting}).
 
+\begin{warn}\index{simplification!of \texttt{case}}%
+  By default only the selector expression ($e$ above) in a
+  \texttt{case}-construct is simplified, in analogy with \texttt{if} (see
+  page~\pageref{if-simp}). Only if that reduces to a constructor is one of
+  the arms of the \texttt{case}-construct exposed and simplified. To ensure
+  full simplification of all parts of a \texttt{case}-construct for datatype
+  $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
+  example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
+\end{warn}
+
 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
 
 Theory \texttt{Arith} declares a generic function \texttt{size} of type