# HG changeset patch
# User wenzelm
# Date 979600963 -3600
# Node ID 5de31ddf9c031a4294aeecf9d1302e9c83a33169
# Parent  b086f4e1722f01d01b9fca23361c60fb6a0b754a
more method_setup examples;

diff -r b086f4e1722f -r 5de31ddf9c03 doc-src/IsarRef/pure.tex
--- 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}
 }