author | paulson |
Mon, 11 Mar 1996 14:04:37 +0100 | |
changeset 1561 | 9ba6d69f7763 |
parent 1560 | 9d001e5f43d8 |
child 1562 | e98c7f6165c9 |
src/HOL/Fun.ML | file | annotate | diff | comparison | revisions |
--- 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];