Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix document generation for Extended_Nat
authorhoelzl
Tue, 12 Nov 2013 20:08:29 +0100
changeset 54419 0c50894fc0d9
parent 54418 3b8e33d1a39a
child 54420 1e6412c82837
fix document generation for Extended_Nat
src/HOL/Library/Extended_Nat.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle