src/HOL/Product_Type.thy
changeset 40590 b994d855dbd2
parent 39302 d7728f65b353
child 40607 30d512bf47a7
     1.1 --- a/src/HOL/Product_Type.thy	Tue Nov 16 13:37:17 2010 -0800
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Nov 16 16:36:57 2010 -0800
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5  subsection {* The @{text unit} type *}
     1.6  
     1.7 -typedef unit = "{True}"
     1.8 +typedef (open) unit = "{True}"
     1.9  proof
    1.10    show "True : ?unit" ..
    1.11  qed
    1.12 @@ -48,7 +48,7 @@
    1.13    "() = Abs_unit True"
    1.14  
    1.15  lemma unit_eq [no_atp]: "u = ()"
    1.16 -  by (induct u) (simp add: unit_def Unity_def)
    1.17 +  by (induct u) (simp add: Unity_def)
    1.18  
    1.19  text {*
    1.20    Simplification procedure for @{thm [source] unit_eq}.  Cannot use