fix document generation for Extended_Nat
authorhoelzl
Tue Nov 12 20:08:29 2013 +0100 (2013-11-12)
changeset 544190c50894fc0d9
parent 54418 3b8e33d1a39a
child 54420 1e6412c82837
fix document generation for Extended_Nat
src/HOL/Library/Extended_Nat.thy
     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)"