--- a/CookBook/Parsing.thy	Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Parsing.thy	Mon Mar 16 00:12:32 2009 +0100
@@ -978,6 +978,42 @@
 
 *}
 
+section {* Methods *}
+
+text {*
+  Methods are one central concept in Isabelle. Methods can be applied with the command
+  \isacommand{apply}. To print out all currently known methods you can use the Isabelle
+  command. 
+*}
+
+print_methods
+
+text {*
+  An example of a very simple method is the following code.
+*}
+
+method_setup %gray foobar_meth = 
+ {* Method.no_args 
+      (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
+        "foobar method"
+
+text {*
+  It defines the method @{text foobar_meth} which takes no arguments and 
+  only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}.
+  It can be applied in the following proof
+*}
+
+lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
+apply(foobar_meth)
+txt {*
+  where it results in the goal state
+
+  \begin{minipage}{\textwidth}
+  @{subgoals}
+  \end{minipage} *}
+(*<*)oops(*>*)
+
+
 (*<*)
 
 chapter {* Parsing *}