--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jul 19 15:37:37 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jul 19 21:47:34 2007 +0200
@@ -590,17 +590,17 @@
\item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
but also offers treatment of character codes; includes
\isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{ExecutableSet}] allows to generate code
+ \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code
for finite sets using lists.
- \item[\isa{ExecutableRat}] \label{exec_rat} implements rational
+ \item[\isa{Executable{\isacharunderscore}Rat}] \label{exec_rat} implements rational
numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
\item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
namly those representable by rational numbers.
- \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers,
+ \item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
which in general will result in higher efficency; pattern
matching with \isa{{\isadigit{0}}} / \isa{Suc}
is eliminated; includes \isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
+ \item[\isa{ML{\isacharunderscore}String}] provides an additional datatype \isa{mlstring};
in the \isa{HOL} default setup, strings in HOL are mapped to list
of \isa{HOL} characters in SML; values of type \isa{mlstring} are
mapped to strings in SML.
@@ -1086,16 +1086,6 @@
for the type constructor's (the constant's) arguments.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ SML\isanewline
-\ \ bool\ true\ false%
-\begin{isamarkuptext}%
-To assert that the existing \qt{bool}, \qt{true} and \qt{false}
- is not used for generated code, we use \isa{{\isasymCODERESERVED}}.
-
- After this setup, code looks quite more readable:%
-\end{isamarkuptext}%
-\isamarkuptrue%
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}%
\begin{isamarkuptext}%