src/HOL/Product_Type.thy
changeset 43866 8a50dc70cbff
parent 43654 3f1a44c2d645
child 44066 d74182c93f04
     1.1 --- a/src/HOL/Product_Type.thy	Sun Jul 17 15:15:58 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sun Jul 17 19:48:02 2011 +0200
     1.3 @@ -84,9 +84,12 @@
     1.4    f} rather than by @{term [source] "%u. f ()"}.
     1.5  *}
     1.6  
     1.7 -lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
     1.8 +lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
     1.9    by (rule ext) simp
    1.10  
    1.11 +lemma UNIV_unit [no_atp]:
    1.12 +  "UNIV = {()}" by auto
    1.13 +
    1.14  instantiation unit :: default
    1.15  begin
    1.16