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