--- a/src/FOL/IFOL.thy Fri Oct 12 12:10:07 2001 +0200
+++ b/src/FOL/IFOL.thy Fri Oct 12 12:11:39 2001 +0200
@@ -119,6 +119,9 @@
setup Simplifier.setup
use "IFOL_lemmas.ML"
+
+declare impE [Pure.elim] iffD1 [Pure.elim] iffD2 [Pure.elim]
+
use "fologic.ML"
use "hypsubstdata.ML"
setup hypsubst_setup