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