changeset 30510 | 4120fc59dd85 |
parent 29752 | ad4e3a577fd3 |
child 30549 | d2d7874648bd |
--- a/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 19:58:26 2009 +0100 @@ -53,7 +53,7 @@ method_setup iff = {* Method.simple_args OuterParse.nat (fn n => fn ctxt => - Method.SIMPLE_METHOD + SIMPLE_METHOD (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) handle Fail _ => no_tac)) *} "iff oracle"