--- a/src/Cube/Example.thy Sun May 15 17:06:35 2011 +0200
+++ b/src/Cube/Example.thy Sun May 15 17:45:53 2011 +0200
@@ -13,19 +13,19 @@
method_setup depth_solve = {*
Attrib.thms >> (fn thms => K (METHOD (fn facts =>
- (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
-*} ""
+ (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
+*}
method_setup depth_solve1 = {*
Attrib.thms >> (fn thms => K (METHOD (fn facts =>
- (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
-*} ""
+ (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
+*}
method_setup strip_asms = {*
Attrib.thms >> (fn thms => K (METHOD (fn facts =>
REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
-*} ""
+*}
subsection {* Simple types *}