| changeset 1762 | 6e481897a811 |
| parent 1760 | 6f41a494f3b1 |
| child 1776 | d7e77cb8ce5c |
--- 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);