src/HOL/Product_Type.thy
changeset 40590 b994d855dbd2
parent 39302 d7728f65b353
child 40607 30d512bf47a7
--- a/src/HOL/Product_Type.thy	Tue Nov 16 13:37:17 2010 -0800
+++ b/src/HOL/Product_Type.thy	Tue Nov 16 16:36:57 2010 -0800
@@ -37,7 +37,7 @@
 
 subsection {* The @{text unit} type *}
 
-typedef unit = "{True}"
+typedef (open) unit = "{True}"
 proof
   show "True : ?unit" ..
 qed
@@ -48,7 +48,7 @@
   "() = Abs_unit True"
 
 lemma unit_eq [no_atp]: "u = ()"
-  by (induct u) (simp add: unit_def Unity_def)
+  by (induct u) (simp add: Unity_def)
 
 text {*
   Simplification procedure for @{thm [source] unit_eq}.  Cannot use