--- 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"];
--- 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
--- 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)"
--- 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}