--- a/doc-src/Codegen/Thy/Adaptation.thy Tue May 19 16:54:55 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed May 20 10:37:36 2009 +0200
@@ -121,8 +121,8 @@
which in general will result in higher efficiency; pattern
matching with @{term "0\<Colon>nat"} / @{const "Suc"}
is eliminated; includes @{theory "Code_Integer"}
- and @{theory "Code_Index"}.
- \item[@{theory "Code_Index"}] provides an additional datatype
+ and @{theory "Code_Numeral"}.
+ \item[@{theory "Code_Numeral"}] provides an additional datatype
@{typ index} which is mapped to target-language built-in integers.
Useful for code setups which involve e.g. indexing of
target-language arrays.
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Tue May 19 16:54:55 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed May 20 10:37:36 2009 +0200
@@ -161,14 +161,14 @@
which in general will result in higher efficiency; pattern
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
- and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
- \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
+ and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}.
+ \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}] provides an additional datatype
\isa{index} which is mapped to target-language built-in integers.
Useful for code setups which involve e.g. indexing of
target-language arrays.
\item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype
- \isa{message{\isacharunderscore}string} which is isomorphic to strings;
- \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
+ \isa{String{\isachardot}literal} which is isomorphic to strings;
+ \isa{String{\isachardot}literal}s are mapped to target-language strings.
Useful for code setups which involve e.g. printing (error) messages.
\end{description}
--- a/doc-src/Codegen/Thy/document/ML.tex Tue May 19 16:54:55 2009 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex Wed May 20 10:37:36 2009 +0200
@@ -124,8 +124,8 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\
- \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+ \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
+ \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
\end{mldecls}
\begin{description}