--- a/doc-src/IsarRef/Thy/document/Introduction.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex Mon Nov 08 00:00:47 2010 +0100
@@ -82,7 +82,7 @@
\medskip Isar commands may be either \emph{proper} document
constructors, or \emph{improper commands}. Some proof methods and
attributes introduced later are classified as improper as well.
- Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful
+ Improper Isar language elements, which are marked by ``\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' in the subsequent chapters; they are often helpful
when developing proof documents, but their use is discouraged for
the final human-readable outcome. Typical examples are diagnostic
commands that print terms or theorems according to the current