diff -r 29e08d527ba1 -r 6e481897a811 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu May 23 15:15:20 1996 +0200
+++ b/src/HOL/Set.ML	Thu May 23 15:16:12 1996 +0200
@@ -137,6 +137,8 @@
 qed "subset_antisym";
 val equalityI = subset_antisym;
 
+AddSIs [equalityI];
+
 (* Equality rules from ZF set theory -- are they appropriate here? *)
 val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
 by (resolve_tac (prems RL [subst]) 1);