src/HOL/Library/Bit.thy
changeset 49834 b27bbb021df1
parent 47108 2a1953f0d20d
child 53063 8f7ac535892f
--- a/src/HOL/Library/Bit.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Bit.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
 
 subsection {* Bits as a datatype *}
 
-typedef (open) bit = "UNIV :: bool set" ..
+typedef bit = "UNIV :: bool set" ..
 
 instantiation bit :: "{zero, one}"
 begin