--- a/src/FOL/IFOL.thy Fri Sep 23 00:10:58 2005 +0200
+++ b/src/FOL/IFOL.thy Fri Sep 23 00:11:10 2005 +0200
@@ -190,7 +190,7 @@
lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
- by rules
+ by iprover
lemmas [sym] = sym iff_sym not_sym iff_not_sym
and [Pure.elim?] = iffD1 iffD2 impE