# HG changeset patch
# User wenzelm
# Date 974483280 -3600
# Node ID 41de88cb2108ca72bba38c93dac57936f00de4c2
# Parent  9efb2fd5399ebdde249dbe1d8534d0357d2593dc
UNIV_witness;

diff -r 9efb2fd5399e -r 41de88cb2108 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Nov 17 18:47:33 2000 +0100
+++ b/src/HOL/Set.ML	Fri Nov 17 18:48:00 2000 +0100
@@ -240,6 +240,11 @@
 Addsimps [UNIV_I];
 AddIs    [UNIV_I];  (*unsafe makes it less likely to cause problems*)
 
+Goal "EX x. x : UNIV";
+by (Simp_tac 1);
+qed "UNIV_witness";
+AddXIs [UNIV_witness];
+
 Goal "A <= UNIV";
 by (rtac subsetI 1);
 by (rtac UNIV_I 1);
@@ -702,6 +707,7 @@
 by (rtac (major RS imageE) 1);
 by (etac minor 1);
 qed "rangeE";
+AddXEs [rangeE];
 
 
 (*** Set reasoning tools ***)