equal
deleted
inserted
replaced
991 text {* |
991 text {* |
992 An example of a very simple method is the following code. |
992 An example of a very simple method is the following code. |
993 *} |
993 *} |
994 |
994 |
995 method_setup %gray foobar_meth = |
995 method_setup %gray foobar_meth = |
996 {* Method.no_args |
996 {* Scan.succeed |
997 (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *} |
997 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
998 "foobar method" |
998 "foobar method" |
999 |
999 |
1000 text {* |
1000 text {* |
1001 It defines the method @{text foobar_meth} which takes no arguments and |
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}. |
1002 only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}. |
1003 It can be applied in the following proof |
1003 It can be applied in the following proof |