--- 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