--- a/doc-src/Codegen/Thy/Refinement.thy Wed Aug 18 11:18:23 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Wed Aug 18 11:18:24 2010 +0200
@@ -116,7 +116,7 @@
"{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
@{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype. The
HOL datatype package by default registers any new datatype with its
- constructors, but this may be changed using @{command
+ constructors, but this may be changed using @{command_def
code_datatype}; the currently chosen constructors can be inspected
using the @{command print_codesetup} command.
@@ -158,7 +158,7 @@
text {*
The same techniques can also be applied to types which are not
specified as datatypes, e.g.~type @{typ int} is originally specified
- as quotient type by means of @{command typedef}, but for code
+ as quotient type by means of @{command_def typedef}, but for code
generation constants allowing construction of binary numeral values
are used as constructors for @{typ int}.
--- a/doc-src/Codegen/Thy/document/Refinement.tex Wed Aug 18 11:18:23 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Wed Aug 18 11:18:24 2010 +0200
@@ -268,7 +268,7 @@
constructor must be of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
\isa{{\isasymtau}}; then \isa{{\isasymkappa}} is its corresponding datatype. The
HOL datatype package by default registers any new datatype with its
- constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
+ constructors, but this may be changed using \indexdef{}{command}{code\_datatype}\hypertarget{command.code-datatype}{\hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}}; the currently chosen constructors can be inspected
using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
Equipped with this, we are able to prove the following equations
@@ -396,7 +396,7 @@
\begin{isamarkuptext}%
The same techniques can also be applied to types which are not
specified as datatypes, e.g.~type \isa{int} is originally specified
- as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
+ as quotient type by means of \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}}, but for code
generation constants allowing construction of binary numeral values
are used as constructors for \isa{int}.