1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 22:49:05 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 23:02:23 2008 +0200
     1.3 @@ -868,9 +868,9 @@
     1.4    methods (see \secref{sec:cases-induct}).
     1.5    
     1.6    \item [@{method (HOL) ind_cases} and @{command (HOL)
     1.7 -  "inductive_cases"}] provide an interface to the internal
     1.8 -  \texttt{mk_cases} operation.  Rules are simplified in an
     1.9 -  unrestricted forward manner.
    1.10 +  "inductive_cases"}] provide an interface to the internal @{ML_text
    1.11 +  mk_cases} operation.  Rules are simplified in an unrestricted
    1.12 +  forward manner.
    1.13  
    1.14    While @{method (HOL) ind_cases} is a proof method to apply the
    1.15    result immediately as elimination rules, @{command (HOL)