# HG changeset patch
# User paulson
# Date 962273685 -7200
# Node ID 7b2f4e6538b42d280691d63418c11d3129c2285a
# Parent  30d46270a42717508127591981ea202d84ebc94f
now uses equalityCE, which usually is more efficent than equalityE

diff -r 30d46270a427 -r 7b2f4e6538b4 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Jun 29 12:14:04 2000 +0200
+++ b/src/HOL/Set.ML	Thu Jun 29 12:14:45 2000 +0200
@@ -210,14 +210,14 @@
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 qed "equalityE";
 
-AddEs [equalityE];
-
 val major::prems = Goal
     "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
 qed "equalityCE";
 
+AddEs [equalityCE];
+
 (*Lemma for creating induction formulae -- for "pattern matching" on p
   To make the induction hypotheses usable, apply "spec" or "bspec" to
   put universal quantifiers over the free variables in p. *)