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