--- a/src/Doc/ProgProve/Basics.thy Tue Mar 12 22:44:03 2013 +0100
+++ b/src/Doc/ProgProve/Basics.thy Wed Mar 13 10:15:01 2013 +0100
@@ -138,8 +138,8 @@
enclosing theory language as the \concept{outer syntax}.
\sem
\begin{warn}
-For reasons of readability, we almost never show the quotation marks in this
-book. Consult the accompanying theory files to see where they need to go.
+In the Isabelle part of the book we show all quotation marks.
+In the Semantics part we omit them for reasons of readability.
\end{warn}
\endsem
%