# HG changeset patch
# User paulson
# Date 951989182 -3600
# Node ID 0e329578b0ef461e5b3c51a48cfc950cc69052f2
# Parent  80855ae484ce35060802bb9617a55910811bf8ee
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
installed them by AddIffs, since they are an important special case of
equalityE.

diff -r 80855ae484ce -r 0e329578b0ef src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Mar 01 20:49:13 2000 +0100
+++ b/src/HOL/Set.ML	Thu Mar 02 10:26:22 2000 +0100
@@ -505,14 +505,15 @@
 AddSEs [singletonE];
 
 Goal "{b} = insert a A = (a = b & A <= {b})";
-by (safe_tac (claset() addSEs [equalityE]));
-by   (ALLGOALS Blast_tac);
+by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "singleton_insert_inj_eq";
 
-Goal "(insert a A = {b} ) = (a = b & A <= {b})";
-by (rtac (singleton_insert_inj_eq RS (eq_sym_conv RS trans)) 1);
+Goal "(insert a A = {b}) = (a = b & A <= {b})";
+by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "singleton_insert_inj_eq'";
 
+AddIffs [singleton_insert_inj_eq, singleton_insert_inj_eq'];
+
 Goal "A <= {x} ==> A={} | A = {x}";
 by (Fast_tac 1);
 qed "subset_singletonD";