1079 |
1079 |
1080 \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which |
1080 \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which |
1081 are not required to have a definition by means of defining equations; |
1081 are not required to have a definition by means of defining equations; |
1082 if needed these are implemented by program abort instead. |
1082 if needed these are implemented by program abort instead. |
1083 |
1083 |
1084 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or |
1084 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or |
1085 with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for |
1085 with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for |
1086 code generation. Usually packages introducing defining equations |
1086 code generation. Usually packages introducing defining equations |
1087 provide a reasonable default setup for selection. |
1087 provide a reasonable default setup for selection. |
1088 |
1088 |
1089 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with |
1089 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with |
1090 option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are |
1090 option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are |
1091 applied as rewrite rules to any defining equation during |
1091 applied as rewrite rules to any defining equation during |
1092 preprocessing. |
1092 preprocessing. |
1093 |
1093 |
1094 \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on |
1094 \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on |
1095 selected defining equations, code generator datatypes and |
1095 selected defining equations, code generator datatypes and |