# HG changeset patch
# User wenzelm
# Date 1330353384 -3600
# Node ID 88f3f5e01d82af0a7152096e4e36ccf3bce44339
# Parent  f800eb467515e6e903a40f2916b75b2fac3c883d
updated generated file;

diff -r f800eb467515 -r 88f3f5e01d82 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Feb 27 15:00:19 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Feb 27 15:36:24 2012 +0100
@@ -2207,7 +2207,7 @@
   \begin{matharray}{rcl}
     \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{command}{try0}\hypertarget{command.HOL.try0}{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{try0}\hypertarget{command.HOL.try0}{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
   \end{matharray}
@@ -2217,7 +2217,7 @@
 \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
 \rail@end
 \rail@begin{6}{}
-\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}[]
+\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@plus
@@ -2304,13 +2304,13 @@
   subgoals can be solved directly by an existing theorem. Duplicate
   lemmas can be detected in this way.
 
-  \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}} attempts to prove a subgoal
+  \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}} attempts to prove a subgoal
   using a combination of standard proof methods (\hyperlink{method.auto}{\mbox{\isa{auto}}},
   \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, etc.).  Additional facts supplied
   via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof methods.
 
   \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
-  using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}).
+  using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try{\isadigit{0}}}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}).
 
   \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal
   using external automatic provers (resolution provers and SMT