--- a/src/Cube/Example.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Cube/Example.thy Fri Mar 13 19:58:26 2009 +0100
@@ -15,18 +15,18 @@
*}
method_setup depth_solve = {*
- Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ Method.thms_args (fn thms => METHOD (fn facts =>
(DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
*} ""
method_setup depth_solve1 = {*
- Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ Method.thms_args (fn thms => METHOD (fn facts =>
(DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
*} ""
method_setup strip_asms = {*
let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
- Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ Method.thms_args (fn thms => METHOD (fn facts =>
REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
end
*} ""