changeset 63680 | 6e1e8b5abbfa |
parent 62390 | 842917225d56 |
child 63762 | 6920b1885eff |
--- a/src/HOL/Word/Word.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/Word/Word.thy Fri Aug 12 17:53:55 2016 +0200 @@ -14,7 +14,7 @@ Word_Miscellaneous begin -text \<open>See @{file "Examples/WordExamples.thy"} for examples.\<close> +text \<open>See \<^file>\<open>Examples/WordExamples.thy\<close> for examples.\<close> subsection \<open>Type definition\<close>