src/HOL/cladata.ML
changeset 9969 4753185f1dd2
parent 9846 bb848beb53f6
child 10197 4ea3ee8de019
     1.1 --- a/src/HOL/cladata.ML	Fri Sep 15 11:34:46 2000 +0200
     1.2 +++ b/src/HOL/cladata.ML	Fri Sep 15 12:39:57 2000 +0200
     1.3 @@ -59,7 +59,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, select_equality] 
     1.8 +val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality] 
     1.9                       addSEs [exE] addEs [allE];
    1.10  
    1.11  val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];