src/Doc/Prog_Prove/Isar.thy

 and after the second \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 < t\<^sub>3"\<close>.
 The command \isakeyword{finally} is short for \isakeyword{also from} \<open>calculation\<close>.
 Therefore the \isakeyword{also} hidden in \isakeyword{finally} sets \<open>calculation\<close>
 to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
 
-For more information on this style of proof see \cite{BauerW-TPHOLs01}.
+For more information on this style of proof see @{cite "BauerW-TPHOLs01"}.
 \fi
 
 \section{Streamlining Proofs}
 
 \subsection{Pattern Matching and Quotations}