diff -r 81caae4fc4fa -r caa7e406056d src/Doc/Isar_Ref/document/style.sty
--- a/src/Doc/Isar_Ref/document/style.sty	Sat Jan 05 17:33:20 2019 +0100
+++ b/src/Doc/Isar_Ref/document/style.sty	Sat Jan 05 20:12:02 2019 +0100
@@ -17,6 +17,7 @@
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
 \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
+\newcommand{\isasymdoublequote}{\texttt{\upshape"}}
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}