# HG changeset patch
# User paulson
# Date 927554008 -7200
# Node ID 89891b0b596f265ad83cef4091f61af5c1844147
# Parent  6b2b4ec581780b36075479dc56225872d9ac51c2
UN_singleton->UN_constant_eq removes clash with other UN_singleton

diff -r 6b2b4ec58178 -r 89891b0b596f src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Mon May 24 15:51:33 1999 +0200
+++ b/src/HOL/Integ/Equiv.ML	Mon May 24 15:53:28 1999 +0200
@@ -125,20 +125,19 @@
 (**** Defining unary operations upon equivalence classes ****)
 
 (* theorem needed to prove UN_equiv_class *)
-goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
+goal Set.thy "!!A. [| a:A; ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
 by (fast_tac (claset() addSEs [equalityE] addSIs [equalityI]) 1);
-qed "UN_singleton_lemma";
-val UN_singleton = ballI RSN (2,UN_singleton_lemma);
+qed "UN_constant_eq";
 
 
-(** These proofs really require the local premises
+(** Could introduce a LOCALE with the assumptions
      equiv A r;  congruent r b
 **)
 
 (*Conversion rule*)
 Goal "[| equiv A r;  congruent r b;  a: A |] \
-\                      ==> (UN x:r^^{a}. b(x)) = b(a)";
-by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
+\     ==> (UN x:r^^{a}. b(x)) = b(a)";
+by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1));
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
 by (Blast_tac 1);
 qed "UN_equiv_class";