# HG changeset patch
# User haftmann
# Date 1279522783 -7200
# Node ID a33ecf47f0a04d93e7c314e2f605e8c3e4ec844a
# Parent  425dd7d97e41fddee5e6c026bb73bcfa5cd92d05
bind and then latex symbols

diff -r 425dd7d97e41 -r a33ecf47f0a0 src/HOL/Extraction/ROOT.ML
--- a/src/HOL/Extraction/ROOT.ML	Sun Jul 18 17:56:04 2010 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Mon Jul 19 08:59:43 2010 +0200
@@ -1,4 +1,4 @@
 (* Examples for program extraction in Higher-Order Logic *)
 
-no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
+no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/UniqueFactorization"];
 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
diff -r 425dd7d97e41 -r a33ecf47f0a0 src/HOL/Extraction/document/root.tex
--- a/src/HOL/Extraction/document/root.tex	Sun Jul 18 17:56:04 2010 +0200
+++ b/src/HOL/Extraction/document/root.tex	Mon Jul 19 08:59:43 2010 +0200
@@ -5,8 +5,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\renewcommand{\isasymguillemotright}{\isamath{\mathbin{>\!\!\!>}}}
-
 \begin{document}
 
 \title{Examples for program extraction in Higher-Order Logic}
@@ -16,6 +14,8 @@
 \nocite{Berger-JAR-2001,Coquand93}
 
 \tableofcontents
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 
 \parindent 0pt\parskip 0.5ex
 
diff -r 425dd7d97e41 -r a33ecf47f0a0 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Sun Jul 18 17:56:04 2010 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Mon Jul 19 08:59:43 2010 +0200
@@ -20,6 +20,9 @@
 notation (xsymbols)
   bind (infixr "\<guillemotright>=" 54)
 
+notation (latex output)
+  bind (infixr "\<bind>" 54)
+
 abbreviation (do_notation)
   bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
 where
@@ -31,6 +34,9 @@
 notation (xsymbols output)
   bind_do (infixr "\<guillemotright>=" 54)
 
+notation (latex output)
+  bind_do (infixr "\<bind>" 54)
+
 nonterminals
   do_binds do_bind
 
@@ -47,6 +53,9 @@
   "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
 
+syntax (latex output)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
+
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"
     == "CONST bind_do t (\<lambda>_. e)"
diff -r 425dd7d97e41 -r a33ecf47f0a0 src/HOL/Library/document/root.tex
--- 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}