equal
deleted
inserted
replaced
56 subsection \<open>Oracle as proof method\<close> |
56 subsection \<open>Oracle as proof method\<close> |
57 |
57 |
58 method_setup iff = |
58 method_setup iff = |
59 \<open>Scan.lift Parse.nat >> (fn n => fn ctxt => |
59 \<open>Scan.lift Parse.nat >> (fn n => fn ctxt => |
60 SIMPLE_METHOD |
60 SIMPLE_METHOD |
61 (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n))) |
61 (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)]) |
62 handle Fail _ => no_tac))\<close> |
62 handle Fail _ => no_tac))\<close> |
63 |
63 |
64 |
64 |
65 lemma "A \<longleftrightarrow> A" |
65 lemma "A \<longleftrightarrow> A" |
66 by (iff 2) |
66 by (iff 2) |