1.1 --- a/src/HOL/Set.ML	Thu May 23 15:15:20 1996 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu May 23 15:16:12 1996 +0200
     1.3 @@ -137,6 +137,8 @@
     1.4  qed "subset_antisym";
     1.5  val equalityI = subset_antisym;
     1.6  
     1.7 +AddSIs [equalityI];
     1.8 +
     1.9  (* Equality rules from ZF set theory -- are they appropriate here? *)
    1.10  val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
    1.11  by (resolve_tac (prems RL [subst]) 1);