# HG changeset patch
# User paulson
# Date 951817268 -3600
# Node ID c7a87e79e9b1f548f6f85f7368f3049d87b932da
# Parent  b470bc28b59ddb0cebb50367a5d68371d131f607
replaced UN_constant, INT_constant by unconditional versions that rewrite
to if-then-else expressions

diff -r b470bc28b59d -r c7a87e79e9b1 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Feb 28 13:39:45 2000 +0100
+++ b/src/HOL/equalities.ML	Tue Feb 29 10:41:08 2000 +0100
@@ -558,13 +558,13 @@
 qed "Inter_image_eq";
 Addsimps [Inter_image_eq];
 
-Goal "u: A ==> (UN y:A. c) = c";
-by (Blast_tac 1);
+Goal "(UN y:A. c) = (if A={} then {} else c)";
+by Auto_tac;
 qed "UN_constant";
 Addsimps[UN_constant];
 
-Goal "u: A ==> (INT y:A. c) = c";
-by (Blast_tac 1);
+Goal "(INT y:A. c) = (if A={} then UNIV else c)";
+by Auto_tac;
 qed "INT_constant";
 Addsimps[INT_constant];