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 58620 7435b6a3f72e
parent 52753 1165f78c16d8
child 59377 056945909f60 
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -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 "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
 
   Consider the simple predicate @{const append} given by these two
   introduction rules:
isabelle