doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 26861 e6fe036ec21d
parent 26854 9b4aec46ad78
child 26895 d066f9db833b
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 23:02:23 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 23:07:15 2008 +0200
     1.3 @@ -871,9 +871,8 @@
     1.4    as would be by the proper \mbox{\isa{induct}} and \mbox{\isa{cases}} proof
     1.5    methods (see \secref{sec:cases-induct}).
     1.6    
     1.7 -  \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}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 +  \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}] provide an interface to the internal \verb|mk_cases| operation.  Rules are simplified in an unrestricted
    1.11 +  forward manner.
    1.12  
    1.13    While \mbox{\isa{ind{\isacharunderscore}cases}} is a proof method to apply the
    1.14    result immediately as elimination rules, \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} provides case split theorems at the theory level