diff -r 56dc95e8b5c5 -r 33d409318266 src/FOL/IFOL.thy
--- 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