# HG changeset patch
# User haftmann
# Date 1206727003 -3600
# Node ID 21504de311979d1606add5b06921e7d73506b880
# Parent  bb0e729be5a4cb48e45a1b8a02c25200dfc7c4d9
some styling

diff -r bb0e729be5a4 -r 21504de31197 doc-src/IsarImplementation/Thy/ML.thy
--- 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"}
diff -r bb0e729be5a4 -r 21504de31197 doc-src/IsarImplementation/Thy/document/ML.tex
--- 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|