src/HOL/Set.ML
changeset 8326 0e329578b0ef
parent 8053 37ebdaf3bb91
child 8839 31da5b9790c0
     1.1 --- a/src/HOL/Set.ML	Wed Mar 01 20:49:13 2000 +0100
     1.2 +++ b/src/HOL/Set.ML	Thu Mar 02 10:26:22 2000 +0100
     1.3 @@ -505,14 +505,15 @@
     1.4  AddSEs [singletonE];
     1.5  
     1.6  Goal "{b} = insert a A = (a = b & A <= {b})";
     1.7 -by (safe_tac (claset() addSEs [equalityE]));
     1.8 -by   (ALLGOALS Blast_tac);
     1.9 +by (blast_tac (claset() addSEs [equalityE]) 1);
    1.10  qed "singleton_insert_inj_eq";
    1.11  
    1.12 -Goal "(insert a A = {b} ) = (a = b & A <= {b})";
    1.13 -by (rtac (singleton_insert_inj_eq RS (eq_sym_conv RS trans)) 1);
    1.14 +Goal "(insert a A = {b}) = (a = b & A <= {b})";
    1.15 +by (blast_tac (claset() addSEs [equalityE]) 1);
    1.16  qed "singleton_insert_inj_eq'";
    1.17  
    1.18 +AddIffs [singleton_insert_inj_eq, singleton_insert_inj_eq'];
    1.19 +
    1.20  Goal "A <= {x} ==> A={} | A = {x}";
    1.21  by (Fast_tac 1);
    1.22  qed "subset_singletonD";