src/HOL/Library/Extended_Nat.thy
changeset 49834 b27bbb021df1
parent 47108 2a1953f0d20d
child 49962 a8cc904a6820
--- a/src/HOL/Library/Extended_Nat.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -25,7 +25,7 @@
   infinity.
 *}
 
-typedef (open) enat = "UNIV :: nat option set" ..
+typedef enat = "UNIV :: nat option set" ..
  
 definition enat :: "nat \<Rightarrow> enat" where
   "enat n = Abs_enat (Some n)"