doc-src/IsarRef/Thy/Proof.thy

   arguments, or a list of theorems, respectively.
 
 %FIXME proper antiquotations
 {\footnotesize
 \begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
-    Method.METHOD (fn facts => foobar_tac))
+ Method.no_args (METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
 \end{verbatim}
 }
 
   Note that mere tactic emulations may ignore the @{text facts}
   parameter above.  Proper proof methods would do something