doc-src/IsarImplementation/Thy/document/ML.tex

 \isadelimML
 %
 \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|,
   continued by an application of a function \verb|g : foo -> bar|,
   and so on.  As a canoncial example, take functions enriching

   \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline%
 \verb|  -> theory -> term * theory| \\
   \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:
 
   \smallskip\begin{mldecls}
   \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
 \verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
 \verb|    (Sign.declare_const []|\isasep\isanewline%
 \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}%
 \isamarkuptrue%
 %

   such that
   \begin{quote}\footnotesize
     \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|
   \end{quote}
   such that