equal
deleted
inserted
replaced
50 |
50 |
51 |
51 |
52 subsection {* Oracle as proof method *} |
52 subsection {* Oracle as proof method *} |
53 |
53 |
54 method_setup iff = {* |
54 method_setup iff = {* |
55 Method.simple_args OuterParse.nat (fn n => fn ctxt => |
55 Scan.lift OuterParse.nat >> (fn n => fn ctxt => |
56 SIMPLE_METHOD |
56 SIMPLE_METHOD |
57 (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) |
57 (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) |
58 handle Fail _ => no_tac)) |
58 handle Fail _ => no_tac)) |
59 *} "iff oracle" |
59 *} "iff oracle" |
60 |
60 |