equal
deleted
inserted
replaced
1097 text {* |
1097 text {* |
1098 It defines the method @{text foo}, 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 "foo"} can be used as follows |
1103 *} |
1103 *} |
1104 |
1104 |
1105 lemma shows "A \<and> B \<Longrightarrow> C \<and> D" |
1105 lemma shows "A \<and> B \<Longrightarrow> C \<and> D" |
1106 apply(foo) |
1106 apply(foo) |
1107 txt {* |
1107 txt {* |