1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jan 19 08:16:43 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jan 19 13:37:24 2009 +0100
     1.3 @@ -3,8 +3,6 @@
     1.4  \def\isabellecontext{HOL{\isacharunderscore}Specific}%
     1.5  %
     1.6  \isadelimtheory
     1.7 -\isanewline
     1.8 -\isanewline
     1.9  %
    1.10  \endisadelimtheory
    1.11  %
    1.12 @@ -1166,21 +1164,21 @@
    1.13    module name onto another.
    1.14  
    1.15    \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
    1.16 -  required to have a definition by means of defining equations; if
    1.17 +  required to have a definition by means of code equations; if
    1.18    needed these are implemented by program abort instead.
    1.19  
    1.20    \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
    1.21 -  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for code
    1.22 -  generation.  Usually packages introducing defining equations provide
    1.23 +  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
    1.24 +  generation.  Usually packages introducing code equations provide
    1.25    a reasonable default setup for selection.
    1.26  
    1.27    \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
    1.28    option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
    1.29 -  applied as rewrite rules to any defining equation during
    1.30 +  applied as rewrite rules to any code equation during
    1.31    preprocessing.
    1.32  
    1.33    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    1.34 -  selected defining equations, code generator datatypes and
    1.35 +  selected code equations, code generator datatypes and
    1.36    preprocessor setup.
    1.37  
    1.38    \end{description}%