# HG changeset patch
# User haftmann
# Date 1279103263 -7200
# Node ID 053d23f089464f5f1089fabf99997048b963a0f8
# Parent  120c6e2d74741d8e7d8ce71197e2e080c696c9cd
self-built symbol for part of bind operator

diff -r 120c6e2d7474 -r 053d23f08946 src/HOL/Extraction/document/root.tex
--- a/src/HOL/Extraction/document/root.tex	Wed Jul 14 09:42:44 2010 +0200
+++ b/src/HOL/Extraction/document/root.tex	Wed Jul 14 12:27:43 2010 +0200
@@ -5,6 +5,8 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
+\renewcommand{\isasymguillemotright}{\isamath{\mathbin{>\!\!\!>}}}
+
 \begin{document}
 
 \title{Examples for program extraction in Higher-Order Logic}