src/FOL/IFOL.thy
changeset 11734 7a21bf539412
parent 11677 ee12f18599e5
child 11747 17a6dcd6f3cf
--- 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