1076   \end{isabelle}

  1076   \end{isabelle}

  1077 

  1077 

  1078   An example of a very simple method is:

  1078   An example of a very simple method is:

  1079 *}

  1079 *}

  1080 

  1080 

  1082  {* Scan.succeed

  1082  {* Scan.succeed

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

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

  1085 

  1085 

  1086 text {*

  1086 text {*

  1087   It defines the method @{text foobar}, which takes no arguments (therefore the

  1087   It defines the method @{text foobar}, which takes no arguments (therefore the

  1088   parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which 

  1088   parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which 

  1089   applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD}

  1089   applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD}

  1090   turns such a tactic into a method. The method @{text "foobar"} can be used as follows

  1090   turns such a tactic into a method. The method @{text "foobar"} can be used as follows

  1091 *}

  1091 *}

  1092 

  1092 

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

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

  1095 txt {*

  1095 txt {*

  1096   where it results in the goal state

  1096   where it results in the goal state

  1097 

  1097 

  1098   \begin{minipage}{\textwidth}

  1098   \begin{minipage}{\textwidth}

  1099   @{subgoals}

  1099   @{subgoals}