# HG changeset patch
# User wenzelm
# Date 1152019828 -7200
# Node ID 05f940b9ef15e160db363be21528b600fa3b657d
# Parent  b97607d4d9a5465c4097e0543b22cc0f80258a22
added 'value';
tuned;

diff -r b97607d4d9a5 -r 05f940b9ef15 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Tue Jul 04 15:26:56 2006 +0200
+++ b/doc-src/IsarRef/logics.tex	Tue Jul 04 15:30:28 2006 +0200
@@ -691,16 +691,19 @@
 
 \subsection{Executable code}
 
-Isabelle/Pure provides a generic infrastructure to support code generation
-from executable specifications, both functional and relational programs.
-Isabelle/HOL instantiates these mechanisms in a way that is amenable to
-end-user applications.  See \cite{isabelle-HOL} for further information (this
-actually covers the new-style theory format as well).
+Isabelle/Pure provides a generic infrastructure to support code
+generation from executable specifications, both functional and
+relational programs.  Isabelle/HOL instantiates these mechanisms in a
+way that is amenable to end-user applications.  See
+\cite{isabelle-HOL} for further information (this actually covers the
+new-style theory format as well).
 
-\indexisarcmd{code-module}\indexisarcmd{code-library}\indexisarcmd{consts-code}\indexisarcmd{types-code}
+\indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library}
+\indexisarcmd{consts-code}\indexisarcmd{types-code}
 \indexisaratt{code}
 
 \begin{matharray}{rcl}
+  \isarcmd{value}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{code_module} & : & \isartrans{theory}{theory} \\
   \isarcmd{code_library} & : & \isartrans{theory}{theory} \\
   \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\
@@ -713,30 +716,20 @@
 \railterm{verblbrace}
 \railterm{verbrbrace}
 
-\railalias{codemodule}{code\_module}
-\railterm{codemodule}
-
-\railalias{codelibrary}{code\_library}
-\railterm{codelibrary}
+\begin{rail}
+'value' term;
 
-\railalias{constscode}{consts\_code}
-\railterm{constscode}
-
-\railalias{typescode}{types\_code}
-\railterm{typescode}
-
-\begin{rail}
-( codemodule | codelibrary ) modespec ? name ? \\
+( 'code\_module' | 'code\_library' ) modespec ? name ? \\
   ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
   'contains' ( ( name '=' term ) + | term + );
 
 modespec : '(' ( name * ) ')';
 
-constscode (codespec +);
+'consts\_code' (codespec +);
 
 codespec : name ( '::' type) ? template attachment ?;
 
-typescode (tycodespec +);
+'types\_code' (tycodespec +);
 
 tycodespec : name template attachment ?;
 
@@ -747,6 +740,11 @@
 'code' (name)?;
 \end{rail}
 
+\begin{descr}
+\item [$\isarkeyword{value}~t$] reads, evaluates and prints a term
+  using the code generator.
+\end{descr}
+
 
 \section{HOLCF}