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