| changeset 17956 | 369e2af8ee45 |
| parent 17002 | fb9261990ffe |
| child 20049 | f48c4a3a34bc |
--- a/src/Provers/quantifier1.ML Fri Oct 21 18:14:32 2005 +0200 +++ b/src/Provers/quantifier1.ML Fri Oct 21 18:14:34 2005 +0200 @@ -104,7 +104,7 @@ in exqu end; fun prove_conv tac thy tu = - Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac)); + Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac)); fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)