--- 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 ***
--- 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{>\!\!\!>}}}
--- 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{>\!\!\!>}}}
--- 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}''}
--- 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}
--- 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