--- a/doc-src/IsarImplementation/Thy/ML.thy Fri Mar 28 18:51:17 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Mar 28 18:56:43 2008 +0100
@@ -308,7 +308,7 @@
(*>*)
text {*
- 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 @{ML_text "x : foo"} which is then transformed
by application of a function @{ML_text "f : foo -> foo"},
@@ -322,7 +322,7 @@
@{ML "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
@{term bar} with type @{typ "foo \<Rightarrow> foo"} and
a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
@@ -333,7 +333,7 @@
(\"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''.
*}
@@ -428,7 +428,7 @@
@{ML_text "y |> fold f [x1, x2, ..., x_n]"} \\
\hspace*{2ex}@{text "\<leadsto>"} @{ML_text "y |> f x1 |> f x2 |> ... |> 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
@{ML_text "f : 'a -> 'b -> 'c * 'b"} to @{ML_text "'a list -> 'b -> 'c list * 'b"}
--- 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|