author haftmann Tue Jul 14 10:54:54 2009 +0200 (2009-07-14) changeset 32000 6f07563dc8a9 parent 31999 cb1f26c0de5b child 32001 fafefd0b341c
updated to changes in sources; tuned
     1.1 --- a/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 10:54:21 2009 +0200
1.2 +++ b/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 10:54:54 2009 +0200
1.3 @@ -153,14 +153,14 @@
1.4    out: \emph{preprocessing}.  In essence, the preprocessor
1.5    consists of two components: a \emph{simpset} and \emph{function transformers}.
1.6
1.7 -  The \emph{simpset} allows to employ the full generality of the Isabelle
1.8 -  simplifier.  Due to the interpretation of theorems
1.9 -  as code equations, rewrites are applied to the right
1.10 -  hand side and the arguments of the left hand side of an
1.11 -  equation, but never to the constant heading the left hand side.
1.12 -  An important special case are \emph{inline theorems} which may be
1.13 -  declared and undeclared using the
1.14 -  \emph{code inline} or \emph{code inline del} attribute respectively.
1.15 +  The \emph{simpset} allows to employ the full generality of the
1.16 +  Isabelle simplifier.  Due to the interpretation of theorems as code
1.17 +  equations, rewrites are applied to the right hand side and the
1.18 +  arguments of the left hand side of an equation, but never to the
1.19 +  constant heading the left hand side.  An important special case are
1.20 +  \emph{unfold theorems} which may be declared and undeclared using
1.21 +  the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
1.22 +  attribute respectively.
1.23
1.24    Some common applications:
1.25  *}
1.26 @@ -173,21 +173,21 @@
1.27       \item replacing non-executable constructs by executable ones:
1.28  *}
1.29
1.30 -lemma %quote [code inline]:
1.31 +lemma %quote [code_inline]:
1.32    "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
1.33
1.34  text {*
1.35       \item eliminating superfluous constants:
1.36  *}
1.37
1.38 -lemma %quote [code inline]:
1.39 +lemma %quote [code_inline]:
1.40    "1 = Suc 0" by simp
1.41
1.42  text {*
1.43       \item replacing executable but inconvenient constructs:
1.44  *}
1.45
1.46 -lemma %quote [code inline]:
1.47 +lemma %quote [code_inline]:
1.48    "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
1.49
1.50  text_raw {*
1.51 @@ -210,10 +210,10 @@
1.52    on code equations.
1.53
1.54    \begin{warn}
1.55 -    The attribute \emph{code unfold}
1.56 -    associated with the @{text "SML code generator"} also applies to
1.57 -    the @{text "generic code generator"}:
1.58 -    \emph{code unfold} implies \emph{code inline}.
1.59 +
1.60 +    Attribute @{attribute code_unfold} also applies to the
1.61 +    preprocessor of the ancient @{text "SML code generator"}; in case
1.62 +    this is not what you intend, use @{attribute code_inline} instead.
1.63    \end{warn}
1.64  *}
1.65

     2.1 --- a/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 10:54:21 2009 +0200
2.2 +++ b/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 10:54:54 2009 +0200
2.3 @@ -124,8 +124,7 @@
2.4  %
2.5  \begin{isamarkuptext}%
2.6  \begin{mldecls}
2.8 -  \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
2.10    \end{mldecls}
2.11
2.12    \begin{description}
2.13 @@ -133,11 +132,6 @@
2.15       reads a constant as a concrete term expression \isa{s}.
2.16
2.17 -  \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
2.18 -     rewrites a code equation \isa{thm} with a simpset \isa{ss};
2.19 -     only arguments and right hand side are rewritten,
2.20 -     not the head of the code equation.
2.21 -
2.22    \end{description}%
2.23  \end{isamarkuptext}%
2.24  \isamarkuptrue%

     3.1 --- a/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 10:54:21 2009 +0200
3.2 +++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 10:54:54 2009 +0200
3.3 @@ -395,14 +395,14 @@
3.4    out: \emph{preprocessing}.  In essence, the preprocessor
3.5    consists of two components: a \emph{simpset} and \emph{function transformers}.
3.6
3.7 -  The \emph{simpset} allows to employ the full generality of the Isabelle
3.8 -  simplifier.  Due to the interpretation of theorems
3.9 -  as code equations, rewrites are applied to the right
3.10 -  hand side and the arguments of the left hand side of an
3.11 -  equation, but never to the constant heading the left hand side.
3.12 -  An important special case are \emph{inline theorems} which may be
3.13 -  declared and undeclared using the
3.14 -  \emph{code inline} or \emph{code inline del} attribute respectively.
3.15 +  The \emph{simpset} allows to employ the full generality of the
3.16 +  Isabelle simplifier.  Due to the interpretation of theorems as code
3.17 +  equations, rewrites are applied to the right hand side and the
3.18 +  arguments of the left hand side of an equation, but never to the
3.19 +  constant heading the left hand side.  An important special case are
3.20 +  \emph{unfold theorems} which may be declared and undeclared using
3.22 +  attribute respectively.
3.23
3.24    Some common applications:%
3.25  \end{isamarkuptext}%
3.26 @@ -421,7 +421,7 @@
3.27  %
3.28  \isatagquote
3.29  \isacommand{lemma}\isamarkupfalse%
3.30 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
3.31 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
3.32  \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.33  \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
3.34  \endisatagquote
3.35 @@ -442,7 +442,7 @@
3.36  %
3.37  \isatagquote
3.38  \isacommand{lemma}\isamarkupfalse%
3.39 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
3.40 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
3.42  \ simp%
3.43  \endisatagquote
3.44 @@ -463,7 +463,7 @@
3.45  %
3.46  \isatagquote
3.47  \isacommand{lemma}\isamarkupfalse%
3.48 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
3.49 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
3.50  \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.51  \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
3.52  \endisatagquote
3.53 @@ -491,10 +491,10 @@
3.54    on code equations.
3.55
3.56    \begin{warn}
3.57 -    The attribute \emph{code unfold}
3.58 -    associated with the \isa{SML\ code\ generator} also applies to
3.59 -    the \isa{generic\ code\ generator}:
3.60 -    \emph{code unfold} implies \emph{code inline}.
3.61 +
3.62 +    Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
3.63 +    preprocessor of the ancient \isa{SML\ code\ generator}; in case