# HG changeset patch # User wenzelm # Date 1288101436 -7200 # Node ID b6fe3b18972546c6e747f32c896c22111876e7bf # Parent 51e026049e4d686d6ab697887d1b1a7c2b7b8897 tuned; diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/ML.thy --- 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 = ... diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/Prelim.thy --- 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 diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/Proof.thy --- 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: *} diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/document/ML.tex --- 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 = ... diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/document/Proof.tex --- 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:%