1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 26 15:55:22 2011 +0100
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 26 16:10:22 2011 +0100
1.3 @@ -24,7 +24,7 @@
1.4 \end{rail}
1.5
1.6 \begin{description}
1.7 -
1.8 +
1.9 \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
1.10 axiomatizes a Gordon/HOL-style type definition in the background
1.11 theory of the current context, depending on a non-emptiness result
1.12 @@ -36,7 +36,7 @@
1.13 multiple interpretations in target contexts. Thus the established
1.14 bijection between the representing set @{text A} and the new type
1.15 @{text t} may semantically depend on local assumptions.
1.16 -
1.17 +
1.18 By default, @{command (HOL) "typedef"} defines both a type @{text t}
1.19 and a set (term constant) of the same name, unless an alternative
1.20 base name is given in parentheses, or the ``@{text "(open)"}''
1.21 @@ -44,7 +44,7 @@
1.22 altogether. The injection from type to set is called @{text Rep_t},
1.23 its inverse @{text Abs_t} --- this may be changed via an explicit
1.24 @{keyword (HOL) "morphisms"} declaration.
1.25 -
1.26 +
1.27 Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
1.28 Abs_t_inverse} provide the most basic characterization as a
1.29 corresponding injection/surjection pair (in both directions). Rules
1.30 @@ -55,7 +55,7 @@
1.31 @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
1.32 on surjectivity; these are already declared as set or type rules for
1.33 the generic @{method cases} and @{method induct} methods.
1.34 -
1.35 +
1.36 An alternative name for the set definition (and other derived
1.37 entities) may be specified in parentheses; the default is to use
1.38 @{text t} as indicated before.
1.39 @@ -77,7 +77,7 @@
1.40 \end{rail}
1.41
1.42 \begin{description}
1.43 -
1.44 +
1.45 \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
1.46 arguments in function applications to be represented canonically
1.47 according to their tuple type structure.
1.48 @@ -140,7 +140,7 @@
1.49 ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
1.50 element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
1.51 for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
1.52 -
1.53 +
1.54 \medskip Two key observations make extensible records in a simply
1.55 typed language like HOL work out:
1.56
1.57 @@ -261,7 +261,7 @@
1.58 \medskip
1.59 \begin{tabular}{lll}
1.60 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
1.61 - @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
1.62 + @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
1.63 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
1.64 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
1.65 @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
1.66 @@ -299,13 +299,13 @@
1.67 @{text t} is a record type as specified above.
1.68
1.69 \begin{enumerate}
1.70 -
1.71 +
1.72 \item Standard conversions for selectors or updates applied to
1.73 record constructor terms are made part of the default Simplifier
1.74 context; thus proofs by reduction of basic operations merely require
1.75 the @{method simp} method without further arguments. These rules
1.76 are available as @{text "t.simps"}, too.
1.77 -
1.78 +
1.79 \item Selectors applied to updated records are automatically reduced
1.80 by an internal simplification procedure, which is also part of the
1.81 standard Simplifier setup.
1.82 @@ -325,7 +325,7 @@
1.83 induct} format (cf.\ the generic proof methods of the same name,
1.84 \secref{sec:cases-induct}). Several variations are available, for
1.85 fixed records, record schemes, more parts etc.
1.86 -
1.87 +
1.88 The generic proof methods are sufficiently smart to pick the most
1.89 sensible rule according to the type of the indicated record
1.90 expression: users just need to apply something like ``@{text "(cases
1.91 @@ -614,7 +614,7 @@
1.92 The mandatory @{text mode} argument specifies the mode of operation
1.93 of the command, which directly corresponds to a complete partial
1.94 order on the result type. By default, the following modes are
1.95 - defined:
1.96 + defined:
1.97
1.98 \begin{description}
1.99 \item @{text option} defines functions that map into the @{type
1.100 @@ -623,7 +623,7 @@
1.101 None} is returned by a recursive call, then the overall result
1.102 must also be @{term None}. This is best achieved through the use of
1.103 the monadic operator @{const "Option.bind"}.
1.104 -
1.105 +
1.106 \item @{text tailrec} defines functions with an arbitrary result
1.107 type and uses the slightly degenerated partial order where @{term
1.108 "undefined"} is the bottom element. Now, monotonicity requires that
1.109 @@ -671,7 +671,7 @@
1.110 \end{rail}
1.111
1.112 \begin{description}
1.113 -
1.114 +
1.115 \item @{command (HOL) "recdef"} defines general well-founded
1.116 recursive functions (using the TFL package), see also
1.117 \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells
1.118 @@ -682,12 +682,12 @@
1.119 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
1.120 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
1.121 Classical reasoner (cf.\ \secref{sec:classical}).
1.122 -
1.123 +
1.124 \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
1.125 proof for leftover termination condition number @{text i} (default
1.126 1) as generated by a @{command (HOL) "recdef"} definition of
1.127 constant @{text c}.
1.128 -
1.129 +
1.130 Note that in most cases, @{command (HOL) "recdef"} is able to finish
1.131 its internal proofs without manual intervention.
1.132
1.133 @@ -984,7 +984,7 @@
1.134
1.135 \item[@{text eval}] takes a term or a list of terms and evaluates
1.136 these terms under the variable assignment found by quickcheck.
1.137 -
1.138 +
1.139 \item[@{text iterations}] sets how many sets of assignments are
1.140 generated for each particular size.
1.141
1.142 @@ -1060,7 +1060,7 @@
1.143 induct} method, @{method induct_tac} does not handle structured rule
1.144 statements, only the compact object-logic conclusion of the subgoal
1.145 being addressed.
1.146 -
1.147 +
1.148 \item @{method (HOL) ind_cases} and @{command (HOL)
1.149 "inductive_cases"} provide an interface to the internal @{ML_text
1.150 mk_cases} operation. Rules are simplified in an unrestricted
1.151 @@ -1224,7 +1224,7 @@
1.152 Serializers take an optional list of arguments in parentheses. For
1.153 \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
1.154 explicit module signatures.
1.155 -
1.156 +
1.157 For \emph{Haskell} a module name prefix may be given using the
1.158 ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
1.159 ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
1.160 @@ -1318,7 +1318,7 @@
1.161 @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
1.162 @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
1.163 @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
1.164 - @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
1.165 + @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
1.166 @{attribute_def (HOL) code} & : & @{text attribute} \\
1.167 \end{matharray}
1.168
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 26 15:55:22 2011 +0100
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 26 16:10:22 2011 +0100
2.3 @@ -44,7 +44,7 @@
2.4 \end{rail}
2.5
2.6 \begin{description}
2.7 -
2.8 +
2.9 \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\isachardoublequote}}}
2.10 axiomatizes a Gordon/HOL-style type definition in the background
2.11 theory of the current context, depending on a non-emptiness result
2.12 @@ -56,7 +56,7 @@
2.13 multiple interpretations in target contexts. Thus the established
2.14 bijection between the representing set \isa{A} and the new type
2.15 \isa{t} may semantically depend on local assumptions.
2.16 -
2.17 +
2.18 By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
2.19 and a set (term constant) of the same name, unless an alternative
2.20 base name is given in parentheses, or the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''
2.21 @@ -64,7 +64,7 @@
2.22 altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
2.23 its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t} --- this may be changed via an explicit
2.24 \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
2.25 -
2.26 +
2.27 Theorems \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t}, \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse} provide the most basic characterization as a
2.28 corresponding injection/surjection pair (in both directions). Rules
2.29 \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} provide a slightly
2.30 @@ -74,7 +74,7 @@
2.31 \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views
2.32 on surjectivity; these are already declared as set or type rules for
2.33 the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
2.34 -
2.35 +
2.36 An alternative name for the set definition (and other derived
2.37 entities) may be specified in parentheses; the default is to use
2.38 \isa{t} as indicated before.
2.39 @@ -98,7 +98,7 @@
2.40 \end{rail}
2.41
2.42 \begin{description}
2.43 -
2.44 +
2.45 \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}complete{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} causes
2.46 arguments in function applications to be represented canonically
2.47 according to their tuple type structure.
2.48 @@ -163,7 +163,7 @@
2.49 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}
2.50 element. In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation
2.51 for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
2.52 -
2.53 +
2.54 \medskip Two key observations make extensible records in a simply
2.55 typed language like HOL work out:
2.56
2.57 @@ -312,13 +312,13 @@
2.58 \isa{t} is a record type as specified above.
2.59
2.60 \begin{enumerate}
2.61 -
2.62 +
2.63 \item Standard conversions for selectors or updates applied to
2.64 record constructor terms are made part of the default Simplifier
2.65 context; thus proofs by reduction of basic operations merely require
2.66 the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules
2.67 are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.
2.68 -
2.69 +
2.70 \item Selectors applied to updated records are automatically reduced
2.71 by an internal simplification procedure, which is also part of the
2.72 standard Simplifier setup.
2.73 @@ -335,7 +335,7 @@
2.74 constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,
2.75 \secref{sec:cases-induct}). Several variations are available, for
2.76 fixed records, record schemes, more parts etc.
2.77 -
2.78 +
2.79 The generic proof methods are sufficiently smart to pick the most
2.80 sensible rule according to the type of the indicated record
2.81 expression: users just need to apply something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' to a certain proof problem.
2.82 @@ -626,14 +626,14 @@
2.83 The mandatory \isa{mode} argument specifies the mode of operation
2.84 of the command, which directly corresponds to a complete partial
2.85 order on the result type. By default, the following modes are
2.86 - defined:
2.87 + defined:
2.88
2.89 \begin{description}
2.90 \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
2.91 non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
2.92 must also be \isa{None}. This is best achieved through the use of
2.93 the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
2.94 -
2.95 +
2.96 \item \isa{tailrec} defines functions with an arbitrary result
2.97 type and uses the slightly degenerated partial order where \isa{{\isaliteral{22}{\isachardoublequote}}undefined{\isaliteral{22}{\isachardoublequote}}} is the bottom element. Now, monotonicity requires that
2.98 if \isa{undefined} is returned by a recursive call, then the
2.99 @@ -680,7 +680,7 @@
2.100 \end{rail}
2.101
2.102 \begin{description}
2.103 -
2.104 +
2.105 \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
2.106 recursive functions (using the TFL package), see also
2.107 \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
2.108 @@ -690,12 +690,12 @@
2.109 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
2.110 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
2.111 Classical reasoner (cf.\ \secref{sec:classical}).
2.112 -
2.113 +
2.114 \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the
2.115 proof for leftover termination condition number \isa{i} (default
2.116 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
2.117 constant \isa{c}.
2.118 -
2.119 +
2.120 Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
2.121 its internal proofs without manual intervention.
2.122
2.123 @@ -1000,6 +1000,9 @@
2.124 \item[\isa{size}] specifies the maximum size of the search space
2.125 for assignment values.
2.126
2.127 + \item[\isa{eval}] takes a term or a list of terms and evaluates
2.128 + these terms under the variable assignment found by quickcheck.
2.129 +
2.130 \item[\isa{iterations}] sets how many sets of assignments are
2.131 generated for each particular size.
2.132
2.133 @@ -1074,7 +1077,7 @@
2.134 methods (see \secref{sec:cases-induct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} does not handle structured rule
2.135 statements, only the compact object-logic conclusion of the subgoal
2.136 being addressed.
2.137 -
2.138 +
2.139 \item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}} provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
2.140 forward manner.
2.141
2.142 @@ -1235,7 +1238,7 @@
2.143 Serializers take an optional list of arguments in parentheses. For
2.144 \emph{SML} and \emph{OCaml}, ``\isa{no{\isaliteral{5F}{\isacharunderscore}}signatures}`` omits
2.145 explicit module signatures.
2.146 -
2.147 +
2.148 For \emph{Haskell} a module name prefix may be given using the
2.149 ``\isa{{\isaliteral{22}{\isachardoublequote}}root{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' argument; ``\isa{string{\isaliteral{5F}{\isacharunderscore}}classes}'' adds a
2.150 ``\verb|deriving (Read, Show)|'' clause to each appropriate
2.151 @@ -1327,7 +1330,7 @@
2.152 \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2.153 \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2.154 \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2.155 - \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2.156 + \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2.157 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
2.158 \end{matharray}
2.159