| changeset 5318 | 72bf8039b53f |
| parent 5316 | 7a8975451a89 |
| child 5336 | 721bf1a13f1a |
--- a/src/HOL/Set.ML Fri Aug 14 12:02:35 1998 +0200 +++ b/src/HOL/Set.ML Fri Aug 14 12:03:01 1998 +0200 @@ -170,7 +170,7 @@ (*Anti-symmetry of the subset relation*) Goal "[| A <= B; B <= A |] ==> A = (B::'a set)"; -br set_ext 1; +by (rtac set_ext 1); by (blast_tac (claset() addIs [subsetD]) 1); qed "subset_antisym"; val equalityI = subset_antisym;