Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Implementation/Eq.thy
changeset 76987 4c275405faae
parent 73764 35d8132633c6 
--- a/src/Doc/Implementation/Eq.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Eq.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -74,10 +74,10 @@
 section \<open>Conversions \label{sec:conv}\<close>
 
 text \<open>
-  The classic article @{cite "paulson:1983"} introduces the concept of
+  The classic article \<^cite>\<open>"paulson:1983"\<close> introduces the concept of
   conversion for Cambridge LCF. This was historically important to implement
   all kinds of ``simplifiers'', but the Isabelle Simplifier is done quite
-  differently, see @{cite \<open>\S9.3\<close> "isabelle-isar-ref"}.
+  differently, see \<^cite>\<open>\<open>\S9.3\<close> in "isabelle-isar-ref"\<close>.
 \<close>
 
 text %mlref \<open>
isabelle