1.1 --- a/src/HOL/Set.ML	Thu Oct 28 19:57:34 1999 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Oct 29 10:10:31 1999 +0200
     1.3 @@ -500,11 +500,15 @@
     1.4  AddSDs [singleton_inject];
     1.5  AddSEs [singletonE];
     1.6  
     1.7 -Goal "{b} = insert a A = (a = b & A <= {a})";
     1.8 +Goal "{b} = insert a A = (a = b & A <= {b})";
     1.9  by (safe_tac (claset() addSEs [equalityE]));
    1.10  by   (ALLGOALS Blast_tac);
    1.11  qed "singleton_insert_inj_eq";
    1.12  
    1.13 +Goal "(insert a A = {b} ) = (a = b & A <= {b})";
    1.14 +by (rtac (singleton_insert_inj_eq RS (eq_sym_conv RS trans)) 1);
    1.15 +qed "singleton_insert_inj_eq'";
    1.16 +
    1.17  Goal "A <= {x} ==> A={} | A = {x}";
    1.18  by (Fast_tac 1);
    1.19  qed "subset_singletonD";