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