# HG changeset patch
# User wenzelm
# Date 995830260 -7200
# Node ID e389e4338604851da073396ecb7ba531a474e6fe
# Parent  9aaab1a160a51df67089633da8bdc4869f56be47
the_equality [intro];

diff -r 9aaab1a160a5 -r e389e4338604 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Sun Jul 22 21:30:21 2001 +0200
+++ b/src/HOL/cladata.ML	Sun Jul 22 21:31:00 2001 +0200
@@ -66,7 +66,7 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality] 
+val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality, the_equality] 
                      addSEs [exE] addEs [allE];
 
 val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];