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/Prelim.thy
changeset 76987 4c275405faae
parent 74561 8e6c973003c8 
--- a/src/Doc/Implementation/Prelim.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Prelim.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -50,7 +50,7 @@
   For example, there would be data for canonical introduction and elimination
   rules for arbitrary operators (depending on the object-logic and
   application), which enables users to perform standard proof steps implicitly
-  (cf.\ the \<open>rule\<close> method @{cite "isabelle-isar-ref"}).
+  (cf.\ the \<open>rule\<close> method \<^cite>\<open>"isabelle-isar-ref"\<close>).
 
   \<^medskip>
   Thus Isabelle/Isar is able to bring forth more and more concepts
isabelle