set_cs now includes singleton_inject
authorpaulson
Mon, 11 Mar 1996 14:04:37 +0100
changeset 1561 9ba6d69f7763
parent 1560 9d001e5f43d8
child 1562 e98c7f6165c9
set_cs now includes singleton_inject
src/HOL/Fun.ML
--- 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];