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/Codegen/Inductive_Predicate.thy
changeset 76987 4c275405faae
parent 72184 881bd98bddee 
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
   which turns inductive specifications into equational ones, from
   which in turn executable code can be generated.  The mechanisms of
   this compiler are described in detail in
-  @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
+  \<^cite>\<open>"Berghofer-Bulwahn-Haftmann:2009:TPHOL"\<close>.
 
   Consider the simple predicate \<^const>\<open>append\<close> given by these two
   introduction rules:
isabelle