# HG changeset patch
# User paulson
# Date 826549477 -3600
# Node ID 9ba6d69f7763be74d693dd4a1631c9b1ddc63b74
# Parent  9d001e5f43d81a2cc7b196cca01e28504145edc7
set_cs now includes singleton_inject

diff -r 9d001e5f43d8 -r 9ba6d69f7763 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];