doc-src/IsarRef/hol.tex
changeset 7987 d9aef93c0e32
parent 7507 e70255cb1035
child 7990 0a604b2fc2b1
     1.1 --- a/doc-src/IsarRef/hol.tex	Sat Oct 30 20:41:30 1999 +0200
     1.2 +++ b/doc-src/IsarRef/hol.tex	Sun Oct 31 15:20:35 1999 +0100
     1.3 @@ -146,8 +146,8 @@
     1.4  \end{descr}
     1.5  
     1.6  See \cite{isabelle-HOL} for more information.  Note that
     1.7 -$\isarkeyword{inductive_cases}$ corresponds to the ML function
     1.8 -\texttt{mk_cases}.
     1.9 +$\isarkeyword{inductive_cases}$ corresponds to the \texttt{mk_cases} ML
    1.10 +function.
    1.11  
    1.12  
    1.13  \section{Proof by induction}