src/Doc/Codegen/Inductive_Predicate.thy

 text \<open>
   The \<open>predicate compiler\<close> is an extension of the code generator
   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:
 \<close>