src/HOL/Library/Extended_Nat.thy
changeset 54419 0c50894fc0d9
parent 54416 7fb88ed6ff3c
child 56777 9c3f0ae99532
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:56 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 20:08:29 2013 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  typedef enat = "UNIV :: nat option set" ..
     1.6  
     1.7 -text {* TODO: introduce enat as coinductive datatype, enat is just of_nat *}
     1.8 +text {* TODO: introduce enat as coinductive datatype, enat is just @{const of_nat} *}
     1.9  
    1.10  definition enat :: "nat \<Rightarrow> enat" where
    1.11    "enat n = Abs_enat (Some n)"