| changeset 10899 | 5de31ddf9c03 |
| parent 10858 | 479dad7b3b41 |
| child 11017 | 241cbdf4134e |
--- a/doc-src/IsarRef/pure.tex Mon Jan 15 10:29:13 2001 +0100 +++ b/doc-src/IsarRef/pure.tex Tue Jan 16 00:22:43 2001 +0100 @@ -442,6 +442,8 @@ \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)) \end{verbatim} }