# HG changeset patch
# User oheimb
# Date 941184631 -7200
# Node ID 7a20317850ab18363e83ba0623f7913c2f89d964
# Parent  964b65b4e4331b29d4c219fbd39560f5d1b23a4e
improved singleton_insert_inj_eq

diff -r 964b65b4e433 -r 7a20317850ab src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Oct 28 19:57:34 1999 +0200
+++ b/src/HOL/Set.ML	Fri Oct 29 10:10:31 1999 +0200
@@ -500,11 +500,15 @@
 AddSDs [singleton_inject];
 AddSEs [singletonE];
 
-Goal "{b} = insert a A = (a = b & A <= {a})";
+Goal "{b} = insert a A = (a = b & A <= {b})";
 by (safe_tac (claset() addSEs [equalityE]));
 by   (ALLGOALS Blast_tac);
 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);
+qed "singleton_insert_inj_eq'";
+
 Goal "A <= {x} ==> A={} | A = {x}";
 by (Fast_tac 1);
 qed "subset_singletonD";