--- a/src/Doc/Locales/Examples3.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Locales/Examples3.thy Sun Jan 15 18:30:18 2023 +0100
@@ -486,13 +486,13 @@
text \<open>More information on locales and their interpretation is
available. For the locale hierarchy of import and interpretation
- dependencies see~@{cite Ballarin2006a}; interpretations in theories
- and proofs are covered in~@{cite Ballarin2006b}. In the latter, I
+ dependencies see~\<^cite>\<open>Ballarin2006a\<close>; interpretations in theories
+ and proofs are covered in~\<^cite>\<open>Ballarin2006b\<close>. In the latter, I
show how interpretation in proofs enables to reason about families
of algebraic structures, which cannot be expressed with locales
directly.
- Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction
+ Haftmann and Wenzel~\<^cite>\<open>HaftmannWenzel2007\<close> overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
facility to generate ML and Haskell code. Classes are sufficient for
@@ -504,14 +504,14 @@
The locales reimplementation for Isabelle 2009 provides, among other
improvements, a clean integration with Isabelle/Isar's local theory
mechanisms, which are described in another paper by Haftmann and
- Wenzel~@{cite HaftmannWenzel2009}.
+ Wenzel~\<^cite>\<open>HaftmannWenzel2009\<close>.
- The original work of Kammüller on locales~@{cite KammullerEtAl1999}
+ The original work of Kammüller on locales~\<^cite>\<open>KammullerEtAl1999\<close>
may be of interest from a historical perspective. My previous
- report on locales and locale expressions~@{cite Ballarin2004a}
+ report on locales and locale expressions~\<^cite>\<open>Ballarin2004a\<close>
describes a simpler form of expressions than available now and is
outdated. The mathematical background on orders and lattices is
- taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
+ taken from Jacobson's textbook on algebra~\<^cite>\<open>\<open>Chapter~8\<close> in Jacobson1985\<close>.
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at