equalityI is now added to default claset
authorberghofe
Thu May 23 15:16:12 1996 +0200 (1996-05-23)
changeset 17626e481897a811
parent 1761 29e08d527ba1
child 1763 fb07e359b59f
equalityI is now added to default claset
src/HOL/Set.ML
     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);