doc-src/ProgProve/Thys/Basics.thy

--- a/doc-src/ProgProve/Thys/Basics.thy	Mon Apr 02 13:47:00 2012 +0200
+++ b/doc-src/ProgProve/Thys/Basics.thy	Mon Apr 02 20:12:10 2012 +0200
@@ -136,10 +136,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}
+\endsem
+%
 *}
 (*<*)
 end