--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:33:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:41:09 2011 +0200
@@ -931,15 +931,20 @@
\begin{matharray}{rcl}
@{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+ @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
\end{matharray}
@{rail "
+ @@{command (HOL) try}
+ ;
+
@@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
@{syntax nat}?
;
+
@@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
;
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri May 27 10:33:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri May 27 10:41:09 2011 +0200
@@ -1277,13 +1277,17 @@
\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}{try\_methods}\hypertarget{command.HOL.try-methods}{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\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}
\begin{railoutput}
+\rail@begin{1}{}
+\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
+\rail@end
\rail@begin{6}{}
-\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
+\rail@term{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
@@ -1362,8 +1366,7 @@
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
\end{railoutput}
- % FIXME try: proper clasimpmod!?
- % FIXME check args "value"
+ % FIXME check args "value"
\begin{description}
@@ -1371,7 +1374,7 @@
be solved directly by an existing theorem. Duplicate lemmas can be detected
in this way.
- \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove a subgoal using a combination
+ \item \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}} attempts to prove a subgoal using a combination
of standard proof methods (\isa{auto}, \isa{simp}, \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