--- a/src/Doc/Tutorial/Inductive/AB.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Inductive/AB.thy Tue Oct 07 22:35:11 2014 +0200
@@ -17,7 +17,7 @@
B &\to& b S \mid a B B \nonumber
\end{eqnarray}
At the end we say a few words about the relationship between
-the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
+the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version.
We start by fixing the alphabet, which consists only of @{term a}'s
and~@{term b}'s:
@@ -283,7 +283,7 @@
text{*
We conclude this section with a comparison of our proof with
Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
-\cite[p.\ts81]{HopcroftUllman}.
+@{cite \<open>p.\ts81\<close> HopcroftUllman}.
For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.