set_cs now includes singleton_inject
authorpaulson
Mon Mar 11 14:04:37 1996 +0100 (1996-03-11)
changeset 15619ba6d69f7763
parent 1560 9d001e5f43d8
child 1562 e98c7f6165c9
set_cs now includes singleton_inject
src/HOL/Fun.ML
     1.1 --- a/src/HOL/Fun.ML	Mon Mar 11 14:03:30 1996 +0100
     1.2 +++ b/src/HOL/Fun.ML	Mon Mar 11 14:04:37 1996 +0100
     1.3 @@ -177,6 +177,7 @@
     1.4              ComplI, IntI, DiffI, UnCI, insertCI] 
     1.5      addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
     1.6      addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
     1.7 +	    make_elim singleton_inject,
     1.8              CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
     1.9      addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
    1.10              subsetD, subsetCE];