equal
deleted
inserted
replaced
88 |
88 |
89 in SIMPLE_METHOD (CHANGED tac) facts end) |
89 in SIMPLE_METHOD (CHANGED tac) facts end) |
90 \<close> |
90 \<close> |
91 |
91 |
92 |
92 |
93 text \<open>The following @{text fails} and @{text succeeds} methods protect the goal from the effect |
93 text \<open>The following \<open>fails\<close> and \<open>succeeds\<close> methods protect the goal from the effect |
94 of a method, instead simply determining whether or not it can be applied to the current goal. |
94 of a method, instead simply determining whether or not it can be applied to the current goal. |
95 The @{text fails} method inverts success, only succeeding if the given method would fail.\<close> |
95 The \<open>fails\<close> method inverts success, only succeeding if the given method would fail.\<close> |
96 |
96 |
97 method_setup fails = |
97 method_setup fails = |
98 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => |
98 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => |
99 let |
99 let |
100 fun fail_tac st' = |
100 fun fail_tac st' = |