src/HOL/Library/document/root.tex

--- a/src/HOL/Library/document/root.tex	Wed Apr 27 10:49:39 2011 +0200
+++ b/src/HOL/Library/document/root.tex	Wed Apr 27 13:21:12 2011 +0200
@@ -21,8 +21,6 @@
 \renewcommand{\isamarkupheader}[1]%
 {\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
 \markright{THEORY~``\isabellecontext''}}
-\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
-\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 
 \input{session}