# HG changeset patch
# User nipkow
# Date 1363166090 -3600
# Node ID df6c246fd3d90135fe013284a4909ad97ae55cfa
# Parent  f4c82c165f589fa309c17b105837150ed15dc9e0
tuned

diff -r f4c82c165f58 -r df6c246fd3d9 src/Doc/ProgProve/Basics.thy
--- a/src/Doc/ProgProve/Basics.thy	Tue Mar 12 19:55:17 2013 +0100
+++ b/src/Doc/ProgProve/Basics.thy	Wed Mar 13 10:14:50 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
 %