| changeset 4068 | 99224854a0ac |
| parent 4067 | 207a7811faa9 |
| child 4503 | 5ed72705c201 |
--- a/doc-src/Logics/HOL.tex Sun Nov 02 13:47:58 1997 +0100 +++ b/doc-src/Logics/HOL.tex Sun Nov 02 14:01:38 1997 +0100 @@ -1632,7 +1632,7 @@ \end{warn} To perform case distinction on a goal containing a \texttt{case}-construct, -the theorem \texttt{split_}$t$\texttt{_case} is provided: +the theorem \texttt{split_}$t$\texttt{_case}\tdx{split_$t$_case} is provided: \[ \begin{array}{@{}rcl@{}} P(t_\mathtt{case}~f@1~\dots~f@m~e) &=&