src/HOL/cladata.ML
changeset 4535 f24cebc299e4
parent 4466 305390f23734
child 4653 d60f76680bf4
     1.1 --- a/src/HOL/cladata.ML	Thu Jan 08 18:08:43 1998 +0100
     1.2 +++ b/src/HOL/cladata.ML	Thu Jan 08 18:09:07 1998 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4                         addSEs [conjE,disjE,impCE,FalseE,iffCE];
     1.5  
     1.6  (*Quantifier rules*)
     1.7 -val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
     1.8 +val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality] 
     1.9                       addSEs [exE] addEs [allE];
    1.10  
    1.11  claset_ref() := HOL_cs;