the_equality [intro];
authorwenzelm
Sun Jul 22 21:31:00 2001 +0200 (2001-07-22)
changeset 11440e389e4338604
parent 11439 9aaab1a160a5
child 11441 54b236801671
the_equality [intro];
src/HOL/cladata.ML
     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)];