--- a/src/HOL/SPARK/Manual/Example_Verification.thy Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy Tue Oct 07 23:12:08 2014 +0200
@@ -23,7 +23,7 @@
We will now explain the usage of the \SPARK{} verification environment by proving
the correctness of an example program. As an example, we use a program for computing
the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
-which has been taken from the book about \SPARK{} by Barnes \cite[\S 11.6]{Barnes}.
+which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}.
*}
section {* Importing \SPARK{} VCs into Isabelle *}
@@ -228,7 +228,7 @@
are trivially proved to be non-negative. Since we are working with non-negative
numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
\textbf{rem}, which spares us an application of theorems @{text zmod_zdiv_equality'}
-and @{text sdiv_pos_pos}. Finally, as noted by Barnes \cite[\S 11.5]{Barnes},
+and @{text sdiv_pos_pos}. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
we can simplify matters by placing the \textbf{assert} statement between
\textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
In the former case, the loop invariant has to be proved only once, whereas in