--- a/doc-src/ProgProve/Thys/document/Basics.tex Mon Apr 02 13:47:00 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Basics.tex Mon Apr 02 20:12:10 2012 +0200
@@ -147,10 +147,13 @@
single identifier can be dropped. When Isabelle prints a syntax error
message, it refers to the HOL syntax as the \concept{inner syntax} and the
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.
-\end{warn}%
+\end{warn}
+\endsem
+%%
\end{isamarkuptext}%
\isamarkuptrue%
%