src/Doc/Logics/document/HOL.tex
changeset 57983 6edc3529bb4e
parent 55415 05f5fdb8d093
child 58318 f95754ca7082
     1.1 --- a/src/Doc/Logics/document/HOL.tex	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/Doc/Logics/document/HOL.tex	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -1709,7 +1709,7 @@
     1.4    the arms of the \texttt{case}-construct exposed and simplified. To ensure
     1.5    full simplification of all parts of a \texttt{case}-construct for datatype
     1.6    $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
     1.7 -  example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
     1.8 +  example by \texttt{delcongs [thm "$t$.case_cong_weak"]}.
     1.9  \end{warn}
    1.10  
    1.11  \subsubsection{The function \cdx{size}}\label{sec:HOL:size}