# HG changeset patch
# User nipkow
# Date 1363166101 -3600
# Node ID b9b273699c26e321a1360f94de75205bb2fa6594
# Parent  950b897f95bb206049d815e3f383ba11fe56c3d5# Parent  df6c246fd3d90135fe013284a4909ad97ae55cfa
merged

diff -r 950b897f95bb -r b9b273699c26 src/Doc/ProgProve/Basics.thy
--- 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
 %