# HG changeset patch
# User berghofe
# Date 832857372 -7200
# Node ID 6e481897a811188985bcd3a939097513dd25987c
# Parent  29e08d527ba1852ca2ccc7347c2037cadf9468a9
equalityI is now added to default claset

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);