# HG changeset patch # User nipkow # Date 1288281265 -7200 # Node ID 997d6fb439a9e5a9ae82f6ace3317fa04c367c9a # Parent e00a2edd1dc6183d3ae1d5edd24955c57c4027bb# Parent be5c622e1de2152dbe4844aa48cf1bb793c92b84 merged diff -r be5c622e1de2 -r 997d6fb439a9 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 28 17:54:09 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 28 17:54:25 2010 +0200 @@ -750,7 +750,7 @@ This can be avoided by \emph{canonical argument order}, which observes certain standard patterns and minimizes adhoc permutations - in their application. In Isabelle/ML, large portions text can be + in their application. In Isabelle/ML, large portions of text can be written without ever using @{text "swap: \ \ \ \ \ \ \"}, or the combinator @{text "C: (\ \ \ \ \) \ (\ \ \ \ \)"} that is not even defined in our library. @@ -787,7 +787,7 @@ to the right: @{text "insert a"} is a function @{text "\ \ \"} to insert a value @{text "a"}. These can be composed naturally as @{text "insert c \ insert b \ insert a"}. The slightly awkward - inversion if the composition order is due to conventional + inversion of the composition order is due to conventional mathematical notation, which can be easily amended as explained below. *} @@ -1138,9 +1138,9 @@ language definition. It was excluded from the SML97 version to avoid its malign impact on ML program semantics, but without providing a viable alternative. Isabelle/ML recovers physical - interruptibility (which an indispensable tool to implement managed - evaluation of command transactions), but requires user code to be - strictly transparent wrt.\ interrupts. + interruptibility (which is an indispensable tool to implement + managed evaluation of command transactions), but requires user code + to be strictly transparent wrt.\ interrupts. \begin{warn} Isabelle/ML user code needs to terminate promptly on interruption, diff -r be5c622e1de2 -r 997d6fb439a9 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 28 17:54:09 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 28 17:54:25 2010 +0200 @@ -948,7 +948,7 @@ This can be avoided by \emph{canonical argument order}, which observes certain standard patterns and minimizes adhoc permutations - in their application. In Isabelle/ML, large portions text can be + in their application. In Isabelle/ML, large portions of text can be written without ever using \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}}, or the combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}} that is not even defined in our library. @@ -983,7 +983,7 @@ to the right: \isa{insert\ a} is a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} to insert a value \isa{a}. These can be composed naturally as \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}. The slightly awkward - inversion if the composition order is due to conventional + inversion of the composition order is due to conventional mathematical notation, which can be easily amended as explained below.% \end{isamarkuptext}% @@ -1450,9 +1450,9 @@ language definition. It was excluded from the SML97 version to avoid its malign impact on ML program semantics, but without providing a viable alternative. Isabelle/ML recovers physical - interruptibility (which an indispensable tool to implement managed - evaluation of command transactions), but requires user code to be - strictly transparent wrt.\ interrupts. + interruptibility (which is an indispensable tool to implement + managed evaluation of command transactions), but requires user code + to be strictly transparent wrt.\ interrupts. \begin{warn} Isabelle/ML user code needs to terminate promptly on interruption,