--- a/src/HOL/Algebra/Multiplicative_Group.thy Fri Dec 29 18:09:38 2017 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Fri Dec 29 19:17:52 2017 +0100
@@ -724,7 +724,7 @@
text \<open>
In this section we show that the multiplicative group of a finite field
is generated by a single element, i.e. it is cyclic. The proof is inspired
- by the first proof given in the survey~\cite{conrad-cyclicity}.
+ by the first proof given in the survey~@{cite "conrad-cyclicity"}.
\<close>
lemma (in group) pow_order_eq_1: