--- a/src/HOL/HOL.thy Fri Oct 12 12:05:02 2001 +0200 +++ b/src/HOL/HOL.thy Fri Oct 12 12:05:46 2001 +0200 @@ -250,6 +250,8 @@ setup Classical.setup setup clasetup +declare impE [CPure.elim] iffD1 [CPure.elim] iffD2 [CPure.elim] + use "blastdata.ML" setup Blast.setup