1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Fri Mar 28 18:51:17 2008 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Mar 28 18:56:43 2008 +0100
     1.3 @@ -308,7 +308,7 @@
     1.4  (*>*)
     1.5  
     1.6  text {*
     1.7 -  Many problems in functional programming can be thought of
     1.8 +  \noindent Many problems in functional programming can be thought of
     1.9    as linear transformations, i.e.~a caluclation starts with a
    1.10    particular value @{ML_text "x : foo"} which is then transformed
    1.11    by application of a function @{ML_text "f : foo -> foo"},
    1.12 @@ -322,7 +322,7 @@
    1.13    @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
    1.14    \end{mldecls}
    1.15  
    1.16 -  Written with naive application, an addition of constant
    1.17 +  \noindent Written with naive application, an addition of constant
    1.18    @{term bar} with type @{typ "foo \<Rightarrow> foo"} and
    1.19    a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
    1.20  
    1.21 @@ -333,7 +333,7 @@
    1.22        (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}
    1.23    \end{mldecls}
    1.24  
    1.25 -  With increasing numbers of applications, this code gets quite
    1.26 +  \noindent With increasing numbers of applications, this code gets quite
    1.27    unreadable.  Further, it is unintuitive that things are
    1.28    written down in the opposite order as they actually ``happen''.
    1.29  *}
    1.30 @@ -428,7 +428,7 @@
    1.31      @{ML_text "y |> fold f [x1, x2, ..., x_n]"} \\
    1.32      \hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 |> f x2 |> ... |> f x_n"}
    1.33    \end{quote}
    1.34 -  The second accumulates side results in a list by lifting
    1.35 +  \noindent The second accumulates side results in a list by lifting
    1.36    a single function
    1.37    \begin{quote}\footnotesize
    1.38      @{ML_text "f : 'a -> 'b -> 'c * 'b"} to @{ML_text "'a list -> 'b -> 'c list * 'b"}

     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Mar 28 18:51:17 2008 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Mar 28 18:56:43 2008 +0100
     2.3 @@ -360,7 +360,7 @@
     2.4  \endisadelimML
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -Many problems in functional programming can be thought of
     2.8 +\noindent Many problems in functional programming can be thought of
     2.9    as linear transformations, i.e.~a caluclation starts with a
    2.10    particular value \verb|x : foo| which is then transformed
    2.11    by application of a function \verb|f : foo -> foo|,
    2.12 @@ -374,7 +374,7 @@
    2.13    \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
    2.14    \end{mldecls}
    2.15  
    2.16 -  Written with naive application, an addition of constant
    2.17 +  \noindent Written with naive application, an addition of constant
    2.18    \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
    2.19    a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
    2.20  
    2.21 @@ -385,7 +385,7 @@
    2.22  \verb|      ("bar", @{typ "foo => foo"}, NoSyn) thy)|
    2.23    \end{mldecls}
    2.24  
    2.25 -  With increasing numbers of applications, this code gets quite
    2.26 +  \noindent With increasing numbers of applications, this code gets quite
    2.27    unreadable.  Further, it is unintuitive that things are
    2.28    written down in the opposite order as they actually ``happen''.%
    2.29  \end{isamarkuptext}%
    2.30 @@ -511,7 +511,7 @@
    2.31      \verb|y |\verb,|,\verb|> fold f [x1, x2, ..., x_n]| \\
    2.32      \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb|> f x2 |\verb,|,\verb|> ... |\verb,|,\verb|> f x_n|
    2.33    \end{quote}
    2.34 -  The second accumulates side results in a list by lifting
    2.35 +  \noindent The second accumulates side results in a list by lifting
    2.36    a single function
    2.37    \begin{quote}\footnotesize
    2.38      \verb|f : 'a -> 'b -> 'c * 'b| to \verb|'a list -> 'b -> 'c list * 'b|