src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Sun Jul 17 15:15:58 2011 +0200
+++ b/src/HOL/Product_Type.thy	Sun Jul 17 19:48:02 2011 +0200
@@ -84,9 +84,12 @@
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
+lemma UNIV_unit [no_atp]:
+  "UNIV = {()}" by auto
+
 instantiation unit :: default
 begin