--- a/src/Doc/Implementation/Local_Theory.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Sun Oct 05 22:47:07 2014 +0200
@@ -90,7 +90,7 @@
reset to the target context. The target now holds definitions for
terms and theorems that stem from the hypothetical @{text
"\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
- particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
+ particular target policy (see @{cite \<open>\S4--5\<close> "Haftmann-Wenzel:2009"}
for details). *}
text %mlref {*
@@ -159,7 +159,7 @@
text {*
%FIXME
- See also \cite{Chaieb-Wenzel:2007}.
+ See also @{cite "Chaieb-Wenzel:2007"}.
*}
end