981 section {* Methods *}

   982 

   983 text {*

   984   Methods are one central concept in Isabelle. Methods can be applied with the command

   985   \isacommand{apply}. To print out all currently known methods you can use the Isabelle

   986   command. 

   987 *}

   988 

   989 print_methods

   990 

   991 text {*

   992   An example of a very simple method is the following code.

   993 *}

   994 

   995 method_setup %gray foobar_meth = 

   996  {* Method.no_args 

   997       (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}

   998         "foobar method"

   999 

  1000 text {*

  1001   It defines the method @{text foobar_meth} which takes no arguments and 

  1002   only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}.

  1003   It can be applied in the following proof

  1004 *}

  1005 

  1006 lemma shows "A \<and> B \<Longrightarrow> C \<and> D"

  1007 apply(foobar_meth)

  1008 txt {*

  1009   where it results in the goal state

  1010 

  1011   \begin{minipage}{\textwidth}

  1012   @{subgoals}

  1013   \end{minipage} *}

  1014 (*<*)oops(*>*)

  1015 

  1016