src/HOL/cladata.ML
changeset 11440 e389e4338604
parent 10906 de95ba2760fe
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/cladata.ML	Sun Jul 22 21:30:21 2001 +0200
     1.2 +++ b/src/HOL/cladata.ML	Sun Jul 22 21:31:00 2001 +0200
     1.3 @@ -66,7 +66,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, some_equality] 
     1.8 +val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality, the_equality] 
     1.9                       addSEs [exE] addEs [allE];
    1.10  
    1.11  val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];