changeset 1561 | 9ba6d69f7763 |
parent 1465 | 5d7a7e439cec |
child 1666 | 5183de4c496d |
--- a/src/HOL/Fun.ML Mon Mar 11 14:03:30 1996 +0100 +++ b/src/HOL/Fun.ML Mon Mar 11 14:04:37 1996 +0100 @@ -177,6 +177,7 @@ ComplI, IntI, DiffI, UnCI, insertCI] addIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE, + make_elim singleton_inject, CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D, subsetD, subsetCE];