# HG changeset patch
# User haftmann
# Date 1282123104 -7200
# Node ID abf95b39d65cbec0eca2477709aef6d18ac48880
# Parent  ec0408c7328b4befc62049f7b718bc9367748f2d
use command_def more consciously

diff -r ec0408c7328b -r abf95b39d65c doc-src/Codegen/Thy/Refinement.thy
--- 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}.
 
diff -r ec0408c7328b -r abf95b39d65c doc-src/Codegen/Thy/document/Refinement.tex
--- 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}.