# HG changeset patch
# User wenzelm
# Date 1303903272 -7200
# Node ID 2777a27506d0d8a56f5df615e82e240e1be04ea9
# Parent  39eefaef816a2ee426a588802b575b9842581a40
predefined LaTeX macros for \<bind> and \<then>;

diff -r 39eefaef816a -r 2777a27506d0 NEWS
--- a/NEWS	Wed Apr 27 10:49:39 2011 +0200
+++ b/NEWS	Wed Apr 27 13:21:12 2011 +0200
@@ -76,11 +76,15 @@
   - Use extended reals instead of positive extended reals.
     INCOMPATIBILITY.
 
+
 *** Document preparation ***
 
 * New term style "isub" as ad-hoc conversion of variables x1, y23 into
 subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
 
+* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
+(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
+
 
 *** ML ***
 
diff -r 39eefaef816a -r 2777a27506d0 doc-src/isabellesym.sty
--- a/doc-src/isabellesym.sty	Wed Apr 27 10:49:39 2011 +0200
+++ b/doc-src/isabellesym.sty	Wed Apr 27 13:21:12 2011 +0200
@@ -356,3 +356,5 @@
 \newcommand{\isasymspacespace}{\isamath{~~}}
 \newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
diff -r 39eefaef816a -r 2777a27506d0 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Wed Apr 27 10:49:39 2011 +0200
+++ b/lib/texinputs/isabellesym.sty	Wed Apr 27 13:21:12 2011 +0200
@@ -356,3 +356,5 @@
 \newcommand{\isasymspacespace}{\isamath{~~}}
 \newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
diff -r 39eefaef816a -r 2777a27506d0 src/HOL/Imperative_HOL/document/root.tex
--- a/src/HOL/Imperative_HOL/document/root.tex	Wed Apr 27 10:49:39 2011 +0200
+++ b/src/HOL/Imperative_HOL/document/root.tex	Wed Apr 27 13:21:12 2011 +0200
@@ -12,9 +12,6 @@
 \pagestyle{myheadings}
 
 
-% symbols
-\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
-
 % canonical quotes
 \newcommand{\qt}[1]{``{#1}''}
 
diff -r 39eefaef816a -r 2777a27506d0 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}
 
diff -r 39eefaef816a -r 2777a27506d0 src/HOL/Proofs/Extraction/document/root.tex
--- a/src/HOL/Proofs/Extraction/document/root.tex	Wed Apr 27 10:49:39 2011 +0200
+++ b/src/HOL/Proofs/Extraction/document/root.tex	Wed Apr 27 13:21:12 2011 +0200
@@ -14,8 +14,6 @@
 \nocite{Berger-JAR-2001,Coquand93}
 
 \tableofcontents
-\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
-\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 
 \parindent 0pt\parskip 0.5ex