--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 26 15:57:16 2010 +0200
@@ -463,7 +463,7 @@
\end{enumerate}
Such weakly structured layout should be use with great care. Here
- is a counter-example involving @{ML_text let} expressions:
+ are some counter-examples involving @{ML_text let} expressions:
\begin{verbatim}
(* WRONG *)
@@ -472,6 +472,10 @@
val y = ...
in ... end
+ fun foo x = let
+ val y = ...
+ in ... end
+
fun foo x =
let
val y = ...
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Tue Oct 26 15:57:16 2010 +0200
@@ -519,7 +519,7 @@
of this module do not care about the declaration order, since that
data structure forces its own arrangement of elements.
- Observe how the @{verbatim merge} operation joins the data slots of
+ Observe how the @{ML_text merge} operation joins the data slots of
the two constituents: @{ML Ord_List.union} prevents duplication of
common data from different branches, thus avoiding the danger of
exponential blowup. Plain list append etc.\ must never be used for
--- a/doc-src/IsarImplementation/Thy/Proof.thy Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Tue Oct 26 15:57:16 2010 +0200
@@ -182,7 +182,7 @@
text {* In the above example, the starting context is derived from the
toplevel theory, which means that fixed variables are internalized
- literally: @{verbatim "x"} is mapped again to @{verbatim "x"}, and
+ literally: @{text "x"} is mapped again to @{text "x"}, and
attempting to fix it again in the subsequent context is an error.
Alternatively, fixed parameters can be renamed explicitly as
follows: *}
@@ -194,7 +194,7 @@
*}
text {* The following ML code can now work with the invented names of
- @{verbatim x1}, @{verbatim x2}, @{verbatim x3}, without depending on
+ @{text x1}, @{text x2}, @{text x3}, without depending on
the details on the system policy for introducing these variants.
Recall that within a proof body the system always invents fresh
``skolem constants'', e.g.\ as follows: *}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Oct 26 15:57:16 2010 +0200
@@ -484,7 +484,7 @@
\end{enumerate}
Such weakly structured layout should be use with great care. Here
- is a counter-example involving \verb|let| expressions:
+ are some counter-examples involving \verb|let| expressions:
\begin{verbatim}
(* WRONG *)
@@ -493,6 +493,10 @@
val y = ...
in ... end
+ fun foo x = let
+ val y = ...
+ in ... end
+
fun foo x =
let
val y = ...
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Tue Oct 26 15:57:16 2010 +0200
@@ -301,7 +301,7 @@
\begin{isamarkuptext}%
In the above example, the starting context is derived from the
toplevel theory, which means that fixed variables are internalized
- literally: \verb|x| is mapped again to \verb|x|, and
+ literally: \isa{x} is mapped again to \isa{x}, and
attempting to fix it again in the subsequent context is an error.
Alternatively, fixed parameters can be renamed explicitly as
follows:%
@@ -332,7 +332,7 @@
%
\begin{isamarkuptext}%
The following ML code can now work with the invented names of
- \verb|x1|, \verb|x2|, \verb|x3|, without depending on
+ \isa{x{\isadigit{1}}}, \isa{x{\isadigit{2}}}, \isa{x{\isadigit{3}}}, without depending on
the details on the system policy for introducing these variants.
Recall that within a proof body the system always invents fresh
``skolem constants'', e.g.\ as follows:%