typedef (open) unit
authorhuffman
Tue Nov 16 16:36:57 2010 -0800 (2010-11-16)
changeset 40590b994d855dbd2
parent 40589 0e77e45d2ffc
child 40591 1c0b5bfa52a1
typedef (open) unit
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 13:37:17 2010 -0800
     1.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 16:36:57 2010 -0800
     1.3 @@ -89,7 +89,7 @@
     1.4  
     1.5  lemma "Rep_unit () = True"
     1.6  nitpick [expect = none]
     1.7 -by (insert Rep_unit) (simp add: unit_def)
     1.8 +by (insert Rep_unit) simp
     1.9  
    1.10  lemma "Rep_unit () = False"
    1.11  nitpick [expect = genuine]
     2.1 --- a/src/HOL/Product_Type.thy	Tue Nov 16 13:37:17 2010 -0800
     2.2 +++ b/src/HOL/Product_Type.thy	Tue Nov 16 16:36:57 2010 -0800
     2.3 @@ -37,7 +37,7 @@
     2.4  
     2.5  subsection {* The @{text unit} type *}
     2.6  
     2.7 -typedef unit = "{True}"
     2.8 +typedef (open) unit = "{True}"
     2.9  proof
    2.10    show "True : ?unit" ..
    2.11  qed
    2.12 @@ -48,7 +48,7 @@
    2.13    "() = Abs_unit True"
    2.14  
    2.15  lemma unit_eq [no_atp]: "u = ()"
    2.16 -  by (induct u) (simp add: unit_def Unity_def)
    2.17 +  by (induct u) (simp add: Unity_def)
    2.18  
    2.19  text {*
    2.20    Simplification procedure for @{thm [source] unit_eq}.  Cannot use