--- a/src/HOL/Library/document/root.tex Sun Jul 18 17:56:04 2010 +0200
+++ b/src/HOL/Library/document/root.tex Mon Jul 19 08:59:43 2010 +0200
@@ -21,7 +21,8 @@
\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}