# HG changeset patch
# User haftmann
# Date 1247561694 -7200
# Node ID 6f07563dc8a97b15b4c923c367d8c87b9657f571
# Parent  cb1f26c0de5bd1b8dd562b35c3036834b52e683f
updated to changes in sources; tuned

diff -r cb1f26c0de5b -r 6f07563dc8a9 doc-src/Codegen/Thy/Program.thy
--- 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}
 *}
 
diff -r cb1f26c0de5b -r 6f07563dc8a9 doc-src/Codegen/Thy/document/ML.tex
--- 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%
diff -r cb1f26c0de5b -r 6f07563dc8a9 doc-src/Codegen/Thy/document/Program.tex
--- 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%