Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 27103 d8549f4d900b
parent 27047 2dcdea037385
child 27124 e02d6e655e60 
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jun 10 15:30:01 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jun 10 15:30:06 2008 +0200
     1.3 @@ -919,7 +919,7 @@
     1.4      \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\
     1.5      \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\
     1.6      \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\
     1.7 -    \indexdef{HOL}{command}{code\_exception}\hypertarget{command.HOL.code-exception}{\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}} & : & \isartrans{theory}{theory} \\
     1.8 +    \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isartrans{theory}{theory} \\
     1.9      \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    1.10      \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
    1.11    \end{matharray}
    1.12 @@ -1070,9 +1070,9 @@
    1.13    \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
    1.14    one module name onto another.
    1.15  
    1.16 -  \item [\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
    1.17 -  are not required to have a definition by a defining equations; these
    1.18 -  are mapped on exceptions instead.
    1.19 +  \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which
    1.20 +  are not required to have a definition by a defining equations;
    1.21 +  if needed these are implemented by program abort instead.
    1.22  
    1.23    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
    1.24    with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
isabelle