--- a/src/HOL/Library/State_Monad.thy Sat Dec 14 17:28:05 2013 +0100
+++ b/src/HOL/Library/State_Monad.thy Sat Dec 14 20:46:36 2013 +0100
@@ -145,7 +145,7 @@
"_sdo_block (_sdo_final e)" => "e"
text {*
- For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
+ For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman.thy"}.
*}
end
--- a/src/HOL/Word/Word.thy Sat Dec 14 17:28:05 2013 +0100
+++ b/src/HOL/Word/Word.thy Sat Dec 14 20:46:36 2013 +0100
@@ -14,7 +14,7 @@
Word_Miscellaneous
begin
-text {* see @{text "Examples/WordExamples.thy"} for examples *}
+text {* See @{file "Examples/WordExamples.thy"} for examples. *}
subsection {* Type definition *}