--- a/doc-src/Codegen/Thy/Program.thy Tue Jul 14 10:54:21 2009 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Tue Jul 14 10:54:54 2009 +0200
@@ -153,14 +153,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the Isabelle
- simplifier. Due to the interpretation of theorems
- as code equations, rewrites are applied to the right
- hand side and the arguments of the left hand side of an
- equation, but never to the constant heading the left hand side.
- An important special case are \emph{inline theorems} which may be
- declared and undeclared using the
- \emph{code inline} or \emph{code inline del} attribute respectively.
+ The \emph{simpset} allows to employ the full generality of the
+ Isabelle simplifier. Due to the interpretation of theorems as code
+ equations, rewrites are applied to the right hand side and the
+ arguments of the left hand side of an equation, but never to the
+ constant heading the left hand side. An important special case are
+ \emph{unfold theorems} which may be declared and undeclared using
+ the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
+ attribute respectively.
Some common applications:
*}
@@ -173,21 +173,21 @@
\item replacing non-executable constructs by executable ones:
*}
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
"x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
text {*
\item eliminating superfluous constants:
*}
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
"1 = Suc 0" by simp
text {*
\item replacing executable but inconvenient constructs:
*}
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
"xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
text_raw {*
@@ -210,10 +210,10 @@
on code equations.
\begin{warn}
- The attribute \emph{code unfold}
- associated with the @{text "SML code generator"} also applies to
- the @{text "generic code generator"}:
- \emph{code unfold} implies \emph{code inline}.
+
+ Attribute @{attribute code_unfold} also applies to the
+ preprocessor of the ancient @{text "SML code generator"}; in case
+ this is not what you intend, use @{attribute code_inline} instead.
\end{warn}
*}
--- a/doc-src/Codegen/Thy/document/ML.tex Tue Jul 14 10:54:21 2009 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex Tue Jul 14 10:54:54 2009 +0200
@@ -124,8 +124,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
- \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+ \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
\end{mldecls}
\begin{description}
@@ -133,11 +132,6 @@
\item \verb|Code.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
- \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
- rewrites a code equation \isa{thm} with a simpset \isa{ss};
- only arguments and right hand side are rewritten,
- not the head of the code equation.
-
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Program.tex Tue Jul 14 10:54:21 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Tue Jul 14 10:54:54 2009 +0200
@@ -395,14 +395,14 @@
out: \emph{preprocessing}. In essence, the preprocessor
consists of two components: a \emph{simpset} and \emph{function transformers}.
- The \emph{simpset} allows to employ the full generality of the Isabelle
- simplifier. Due to the interpretation of theorems
- as code equations, rewrites are applied to the right
- hand side and the arguments of the left hand side of an
- equation, but never to the constant heading the left hand side.
- An important special case are \emph{inline theorems} which may be
- declared and undeclared using the
- \emph{code inline} or \emph{code inline del} attribute respectively.
+ The \emph{simpset} allows to employ the full generality of the
+ Isabelle simplifier. Due to the interpretation of theorems as code
+ equations, rewrites are applied to the right hand side and the
+ arguments of the left hand side of an equation, but never to the
+ constant heading the left hand side. An important special case are
+ \emph{unfold theorems} which may be declared and undeclared using
+ the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
+ attribute respectively.
Some common applications:%
\end{isamarkuptext}%
@@ -421,7 +421,7 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagquote
@@ -442,7 +442,7 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagquote
@@ -463,7 +463,7 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagquote
@@ -491,10 +491,10 @@
on code equations.
\begin{warn}
- The attribute \emph{code unfold}
- associated with the \isa{SML\ code\ generator} also applies to
- the \isa{generic\ code\ generator}:
- \emph{code unfold} implies \emph{code inline}.
+
+ Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
+ preprocessor of the ancient \isa{SML\ code\ generator}; in case
+ this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%