equal
deleted
inserted
replaced
16 method_setup depth_solve1 = |
16 method_setup depth_solve1 = |
17 \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts => |
17 \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts => |
18 (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close> |
18 (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close> |
19 |
19 |
20 method_setup strip_asms = |
20 method_setup strip_asms = |
21 \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts => |
21 \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => |
22 REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN |
22 REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN |
23 DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))\<close> |
23 DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))\<close> |
24 |
24 |
25 |
25 |
26 subsection \<open>Simple types\<close> |
26 subsection \<open>Simple types\<close> |
27 |
27 |
28 schematic_lemma "A:* \<turnstile> A\<rightarrow>A : ?T" |
28 schematic_lemma "A:* \<turnstile> A\<rightarrow>A : ?T" |