equal
deleted
inserted
replaced
897 arguments, or a list of theorems, respectively. |
897 arguments, or a list of theorems, respectively. |
898 |
898 |
899 %FIXME proper antiquotations |
899 %FIXME proper antiquotations |
900 {\footnotesize |
900 {\footnotesize |
901 \begin{verbatim} |
901 \begin{verbatim} |
902 Method.no_args (Method.METHOD (fn facts => foobar_tac)) |
902 Method.no_args (METHOD (fn facts => foobar_tac)) |
903 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) |
903 Method.thms_args (fn thms => METHOD (fn facts => foobar_tac)) |
904 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) |
904 Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac)) |
905 Method.thms_ctxt_args (fn thms => fn ctxt => |
905 Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac)) |
906 Method.METHOD (fn facts => foobar_tac)) |
|
907 \end{verbatim} |
906 \end{verbatim} |
908 } |
907 } |
909 |
908 |
910 Note that mere tactic emulations may ignore the \isa{facts} |
909 Note that mere tactic emulations may ignore the \isa{facts} |
911 parameter above. Proper proof methods would do something |
910 parameter above. Proper proof methods would do something |