# HG changeset patch
# User huffman
# Date 1289954217 28800
# Node ID b994d855dbd28e1dd9ceb382258453ffe39d3cfa
# Parent  0e77e45d2ffc489723107ab57dd3fc05827fdb2e
typedef (open) unit

diff -r 0e77e45d2ffc -r b994d855dbd2 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 13:37:17 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 16:36:57 2010 -0800
@@ -89,7 +89,7 @@
 
 lemma "Rep_unit () = True"
 nitpick [expect = none]
-by (insert Rep_unit) (simp add: unit_def)
+by (insert Rep_unit) simp
 
 lemma "Rep_unit () = False"
 nitpick [expect = genuine]
diff -r 0e77e45d2ffc -r b994d855dbd2 src/HOL/Product_Type.thy
--- 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