src/HOL/Library/document/root.tex

 \newpage
 
 \renewcommand{\isamarkupheader}[1]%
 {\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
 \markright{THEORY~``\isabellecontext''}}
-\renewcommand{\isasymguillemotright}{$\gg$}
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 
 \input{session}
 
 \pagestyle{headings}
 \bibliographystyle{abbrv}