
diff -r 9dd88f3aa8e0 -r 7a21bf539412 src/FOL/IFOL.thy
--- 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




