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