# HG changeset patch
# User hoelzl
# Date 1384283309 -3600
# Node ID 0c50894fc0d986a3534da9c23417db083f40bd9f
# Parent  3b8e33d1a39a45744a362571b50516734b01b6ec
fix document generation for Extended_Nat

diff -r 3b8e33d1a39a -r 0c50894fc0d9 src/HOL/Library/Extended_Nat.thy
--- 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)"