predefined LaTeX macros for \<bind> and \<then>;
authorwenzelm
Wed Apr 27 13:21:12 2011 +0200 (2011-04-27)
changeset 424842777a27506d0
parent 42483 39eefaef816a
child 42485 4faf82d12b19
child 42497 89acb654d8eb
child 42499 adfa6ad43ab6
predefined LaTeX macros for \<bind> and \<then>;
NEWS
doc-src/isabellesym.sty
lib/texinputs/isabellesym.sty
src/HOL/Imperative_HOL/document/root.tex
src/HOL/Library/document/root.tex
src/HOL/Proofs/Extraction/document/root.tex
     1.1 --- a/NEWS	Wed Apr 27 10:49:39 2011 +0200
     1.2 +++ b/NEWS	Wed Apr 27 13:21:12 2011 +0200
     1.3 @@ -76,11 +76,15 @@
     1.4    - Use extended reals instead of positive extended reals.
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +
     1.8  *** Document preparation ***
     1.9  
    1.10  * New term style "isub" as ad-hoc conversion of variables x1, y23 into
    1.11  subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
    1.12  
    1.13 +* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
    1.14 +(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
    1.15 +
    1.16  
    1.17  *** ML ***
    1.18  
     2.1 --- a/doc-src/isabellesym.sty	Wed Apr 27 10:49:39 2011 +0200
     2.2 +++ b/doc-src/isabellesym.sty	Wed Apr 27 13:21:12 2011 +0200
     2.3 @@ -356,3 +356,5 @@
     2.4  \newcommand{\isasymspacespace}{\isamath{~~}}
     2.5  \newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
     2.6  \newcommand{\isasymsome}{\isamath{\epsilon\,}}
     2.7 +\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
     2.8 +\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
     3.1 --- a/lib/texinputs/isabellesym.sty	Wed Apr 27 10:49:39 2011 +0200
     3.2 +++ b/lib/texinputs/isabellesym.sty	Wed Apr 27 13:21:12 2011 +0200
     3.3 @@ -356,3 +356,5 @@
     3.4  \newcommand{\isasymspacespace}{\isamath{~~}}
     3.5  \newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
     3.6  \newcommand{\isasymsome}{\isamath{\epsilon\,}}
     3.7 +\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
     3.8 +\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
     4.1 --- a/src/HOL/Imperative_HOL/document/root.tex	Wed Apr 27 10:49:39 2011 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/document/root.tex	Wed Apr 27 13:21:12 2011 +0200
     4.3 @@ -12,9 +12,6 @@
     4.4  \pagestyle{myheadings}
     4.5  
     4.6  
     4.7 -% symbols
     4.8 -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
     4.9 -
    4.10  % canonical quotes
    4.11  \newcommand{\qt}[1]{``{#1}''}
    4.12  
     5.1 --- a/src/HOL/Library/document/root.tex	Wed Apr 27 10:49:39 2011 +0200
     5.2 +++ b/src/HOL/Library/document/root.tex	Wed Apr 27 13:21:12 2011 +0200
     5.3 @@ -21,8 +21,6 @@
     5.4  \renewcommand{\isamarkupheader}[1]%
     5.5  {\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
     5.6  \markright{THEORY~``\isabellecontext''}}
     5.7 -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
     5.8 -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
     5.9  
    5.10  \input{session}
    5.11  
     6.1 --- a/src/HOL/Proofs/Extraction/document/root.tex	Wed Apr 27 10:49:39 2011 +0200
     6.2 +++ b/src/HOL/Proofs/Extraction/document/root.tex	Wed Apr 27 13:21:12 2011 +0200
     6.3 @@ -14,8 +14,6 @@
     6.4  \nocite{Berger-JAR-2001,Coquand93}
     6.5  
     6.6  \tableofcontents
     6.7 -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
     6.8 -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
     6.9  
    6.10  \parindent 0pt\parskip 0.5ex
    6.11