equal
deleted
inserted
replaced
1093 {* Scan.succeed |
1093 {* Scan.succeed |
1094 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
1094 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
1095 "foo method for conjE and conjI" |
1095 "foo method for conjE and conjI" |
1096 |
1096 |
1097 text {* |
1097 text {* |
1098 It defines the method @{text foobar}, which takes no arguments (therefore the |
1098 It defines the method @{text foo}, which takes no arguments (therefore the |
1099 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which |
1099 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which |
1100 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function |
1100 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function |
1101 @{ML [index] SIMPLE_METHOD} |
1101 @{ML [index] SIMPLE_METHOD} |
1102 turns such a tactic into a method. The method @{text "foobar"} can be used as follows |
1102 turns such a tactic into a method. The method @{text "foobar"} can be used as follows |
1103 *} |
1103 *} |