# HG changeset patch
# User wenzelm
# Date 1002881499 -7200
# Node ID 7a21bf539412bf3b48cea7d7c9c53f97be3f6346
# Parent  9dd88f3aa8e0f22da0f0f70447304c43c38fea06
declare impE iffD1 iffD2 ad elim of Pure;

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