equal
deleted
inserted
replaced
17 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => |
17 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => |
18 (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close> |
18 (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close> |
19 |
19 |
20 method_setup strip_asms = |
20 method_setup strip_asms = |
21 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => |
21 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => |
22 REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN |
22 REPEAT (resolve_tac ctxt @{thms strip_b strip_s} 1 THEN |
23 DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close> |
23 DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close> |
24 |
24 |
25 |
25 |
26 subsection \<open>Simple types\<close> |
26 subsection \<open>Simple types\<close> |
27 |
27 |