UNIV_witness;

--- 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 ***)