# HG changeset patch
# User wenzelm
# Date 1425662492 -3600
# Node ID 6c0e70b011118b8adf4f1c8bd0de2fa24b488ba3
# Parent  920889b0788e03a3eb7d50dd83a6e986e77cbc5f
tuned;

diff -r 920889b0788e -r 6c0e70b01111 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Fri Mar 06 17:32:20 2015 +0100
+++ b/src/Doc/Implementation/ML.thy	Fri Mar 06 18:21:32 2015 +0100
@@ -92,7 +92,7 @@
   \end{verbatim}
 
   As in regular typography, there is some extra space \emph{before}
-  section headings that are adjacent to plain text, bit not other headings
+  section headings that are adjacent to plain text, but not other headings
   as in the example above.
 
   \medskip The precise wording of the prose text given in these
@@ -585,10 +585,9 @@
   graph.}
 
   \medskip The next example shows how to embed ML into Isar proofs, using
-  @{command_ref "ML_prf"} instead of Instead of @{command_ref "ML"}.
-  As illustrated below, the effect on the ML environment is local to
-  the whole proof body, but ignoring the block structure.
-\<close>
+  @{command_ref "ML_prf"} instead of @{command_ref "ML"}. As illustrated
+  below, the effect on the ML environment is local to the whole proof body,
+  but ignoring the block structure. \<close>
 
 notepad
 begin