doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 28788 ff9d8a8932e4
parent 28687 150a8a1eae1a
child 29113 fb31b7a6c858
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Nov 13 22:44:40 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Nov 13 22:45:12 2008 +0100
     1.3 @@ -30,8 +30,8 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{matharray}{rcl}
     1.7 -    \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\
     1.8 -    \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isartrans{theory}{proof(prove)} \\
     1.9 +    \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.10 +    \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
    1.11    \end{matharray}
    1.12  
    1.13    \begin{rail}
    1.14 @@ -48,17 +48,18 @@
    1.15      ;
    1.16    \end{rail}
    1.17  
    1.18 -  \begin{descr}
    1.19 +  \begin{description}
    1.20    
    1.21 -  \item [\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] is similar to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of
    1.22 -  Isabelle/Pure (see \secref{sec:types-pure}), but also declares type
    1.23 -  arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an
    1.24 -  actual HOL type constructor.   %FIXME check, update
    1.25 +  \item \hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} is similar
    1.26 +  to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see
    1.27 +  \secref{sec:types-pure}), but also declares type arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an actual HOL type
    1.28 +  constructor.  %FIXME check, update
    1.29    
    1.30 -  \item [\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}] sets up a goal stating non-emptiness of the set \isa{A}.
    1.31 -  After finishing the proof, the theory will be augmented by a
    1.32 -  Gordon/HOL-style type definition, which establishes a bijection
    1.33 -  between the representing set \isa{A} and the new type \isa{t}.
    1.34 +  \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}} sets up
    1.35 +  a goal stating non-emptiness of the set \isa{A}.  After finishing
    1.36 +  the proof, the theory will be augmented by a Gordon/HOL-style type
    1.37 +  definition, which establishes a bijection between the representing
    1.38 +  set \isa{A} and the new type \isa{t}.
    1.39    
    1.40    Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base
    1.41    name may be given in parentheses).  The injection from type to set
    1.42 @@ -80,7 +81,7 @@
    1.43    declaration suppresses a separate constant definition for the
    1.44    representing set.
    1.45  
    1.46 -  \end{descr}
    1.47 +  \end{description}
    1.48  
    1.49    Note that raw type declarations are rarely used in practice; the
    1.50    main application is with experimental (or even axiomatic!) theory
    1.51 @@ -95,7 +96,7 @@
    1.52  %
    1.53  \begin{isamarkuptext}%
    1.54  \begin{matharray}{rcl}
    1.55 -    \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
    1.56 +    \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
    1.57    \end{matharray}
    1.58  
    1.59    \begin{rail}
    1.60 @@ -103,19 +104,19 @@
    1.61      ;
    1.62    \end{rail}
    1.63  
    1.64 -  \begin{descr}
    1.65 +  \begin{description}
    1.66    
    1.67 -  \item [\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] puts expressions of
    1.68 -  low-level tuple types into canonical form as specified by the
    1.69 -  arguments given; the \isa{i}-th collection of arguments refers to
    1.70 -  occurrences in premise \isa{i} of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function
    1.71 -  applications to be represented canonically according to their tuple
    1.72 -  type structure.
    1.73 +  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}} puts expressions of low-level tuple types into
    1.74 +  canonical form as specified by the arguments given; the \isa{i}-th
    1.75 +  collection of arguments refers to occurrences in premise \isa{i}
    1.76 +  of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
    1.77 +  arguments in function applications to be represented canonically
    1.78 +  according to their tuple type structure.
    1.79  
    1.80    Note that these operations tend to invent funny names for new local
    1.81    parameters to be introduced.
    1.82  
    1.83 -  \end{descr}%
    1.84 +  \end{description}%
    1.85  \end{isamarkuptext}%
    1.86  \isamarkuptrue%
    1.87  %
    1.88 @@ -204,7 +205,7 @@
    1.89  %
    1.90  \begin{isamarkuptext}%
    1.91  \begin{matharray}{rcl}
    1.92 -    \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isartrans{theory}{theory} \\
    1.93 +    \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.94    \end{matharray}
    1.95  
    1.96    \begin{rail}
    1.97 @@ -212,10 +213,9 @@
    1.98      ;
    1.99    \end{rail}
   1.100  
   1.101 -  \begin{descr}
   1.102 +  \begin{description}
   1.103  
   1.104 -  \item [\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}\ {\isacharplus}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}] defines
   1.105 -  extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}},
   1.106 +  \item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}\ {\isacharplus}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} defines extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}},
   1.107    derived from the optional parent record \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} by adding new
   1.108    field components \isa{{\isachardoublequote}c\isactrlsub i\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} etc.
   1.109  
   1.110 @@ -236,7 +236,7 @@
   1.111    type abbreviation for the fixed record type \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}}, likewise is \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharcomma}\ {\isasymzeta}{\isacharparenright}\ t{\isacharunderscore}scheme{\isachardoublequote}} made an abbreviation for
   1.112    \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}}.
   1.113  
   1.114 -  \end{descr}%
   1.115 +  \end{description}%
   1.116  \end{isamarkuptext}%
   1.117  \isamarkuptrue%
   1.118  %
   1.119 @@ -364,8 +364,8 @@
   1.120  %
   1.121  \begin{isamarkuptext}%
   1.122  \begin{matharray}{rcl}
   1.123 -    \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
   1.124 -  \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{proof} \\
   1.125 +    \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.126 +  \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   1.127    \end{matharray}
   1.128  
   1.129    \begin{rail}
   1.130 @@ -379,16 +379,16 @@
   1.131      cons: name (type *) mixfix?
   1.132    \end{rail}
   1.133  
   1.134 -  \begin{descr}
   1.135 +  \begin{description}
   1.136  
   1.137 -  \item [\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}] defines inductive datatypes in
   1.138 +  \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
   1.139    HOL.
   1.140  
   1.141 -  \item [\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
   1.142 +  \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}} represents existing types as
   1.143    inductive ones, generating the standard infrastructure of derived
   1.144    concepts (primitive recursion etc.).
   1.145  
   1.146 -  \end{descr}
   1.147 +  \end{description}
   1.148  
   1.149    The induction and exhaustion theorems generated provide case names
   1.150    according to the constructors involved, while parameters are named
   1.151 @@ -409,10 +409,10 @@
   1.152  %
   1.153  \begin{isamarkuptext}%
   1.154  \begin{matharray}{rcl}
   1.155 -    \indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.156 -    \indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.157 -    \indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   1.158 -    \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   1.159 +    \indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.160 +    \indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.161 +    \indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   1.162 +    \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   1.163    \end{matharray}
   1.164  
   1.165    \begin{rail}
   1.166 @@ -429,12 +429,12 @@
   1.167      'termination' ( term )?
   1.168    \end{rail}
   1.169  
   1.170 -  \begin{descr}
   1.171 +  \begin{description}
   1.172  
   1.173 -  \item [\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}] defines primitive recursive
   1.174 +  \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
   1.175    functions over datatypes, see also \cite{isabelle-HOL}.
   1.176  
   1.177 -  \item [\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}] defines functions by general
   1.178 +  \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
   1.179    wellfounded recursion. A detailed description with examples can be
   1.180    found in \cite{isabelle-function}. The function is specified by a
   1.181    set of (possibly conditional) recursive equations with arbitrary
   1.182 @@ -447,18 +447,17 @@
   1.183    predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
   1.184    command can then be used to establish that the function is total.
   1.185  
   1.186 -  \item [\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}] is a shorthand notation for
   1.187 -  ``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by
   1.188 -  automated proof attempts regarding pattern matching and termination.
   1.189 -  See \cite{isabelle-function} for further details.
   1.190 +  \item \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} is a shorthand notation for ``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by automated
   1.191 +  proof attempts regarding pattern matching and termination.  See
   1.192 +  \cite{isabelle-function} for further details.
   1.193  
   1.194 -  \item [\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f}] commences a
   1.195 +  \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
   1.196    termination proof for the previously defined function \isa{f}.  If
   1.197    this is omitted, the command refers to the most recent function
   1.198    definition.  After the proof is closed, the recursive equations and
   1.199    the induction principle is established.
   1.200  
   1.201 -  \end{descr}
   1.202 +  \end{description}
   1.203  
   1.204    %FIXME check
   1.205  
   1.206 @@ -481,31 +480,31 @@
   1.207    The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
   1.208    options.
   1.209  
   1.210 -  \begin{descr}
   1.211 +  \begin{description}
   1.212  
   1.213 -  \item [\isa{sequential}] enables a preprocessor which
   1.214 -  disambiguates overlapping patterns by making them mutually disjoint.
   1.215 -  Earlier equations take precedence over later ones.  This allows to
   1.216 -  give the specification in a format very similar to functional
   1.217 -  programming.  Note that the resulting simplification and induction
   1.218 -  rules correspond to the transformed specification, not the one given
   1.219 +  \item \isa{sequential} enables a preprocessor which disambiguates
   1.220 +  overlapping patterns by making them mutually disjoint.  Earlier
   1.221 +  equations take precedence over later ones.  This allows to give the
   1.222 +  specification in a format very similar to functional programming.
   1.223 +  Note that the resulting simplification and induction rules
   1.224 +  correspond to the transformed specification, not the one given
   1.225    originally. This usually means that each equation given by the user
   1.226    may result in several theroems.  Also note that this automatic
   1.227    transformation only works for ML-style datatype patterns.
   1.228  
   1.229 -  \item [\isa{domintros}] enables the automated generation of
   1.230 +  \item \isa{domintros} enables the automated generation of
   1.231    introduction rules for the domain predicate. While mostly not
   1.232    needed, they can be helpful in some proofs about partial functions.
   1.233  
   1.234 -  \item [\isa{tailrec}] generates the unconstrained recursive
   1.235 +  \item \isa{tailrec} generates the unconstrained recursive
   1.236    equations even without a termination proof, provided that the
   1.237    function is tail-recursive. This currently only works
   1.238  
   1.239 -  \item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a
   1.240 +  \item \isa{{\isachardoublequote}default\ d{\isachardoublequote}} allows to specify a default value for a
   1.241    (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}
   1.242    whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.
   1.243  
   1.244 -  \end{descr}%
   1.245 +  \end{description}%
   1.246  \end{isamarkuptext}%
   1.247  \isamarkuptrue%
   1.248  %
   1.249 @@ -515,9 +514,9 @@
   1.250  %
   1.251  \begin{isamarkuptext}%
   1.252  \begin{matharray}{rcl}
   1.253 -    \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
   1.254 -    \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\
   1.255 -    \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
   1.256 +    \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
   1.257 +    \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
   1.258 +    \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
   1.259    \end{matharray}
   1.260  
   1.261    \begin{rail}
   1.262 @@ -527,21 +526,21 @@
   1.263      ;
   1.264    \end{rail}
   1.265  
   1.266 -  \begin{descr}
   1.267 +  \begin{description}
   1.268  
   1.269 -  \item [\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
   1.270 +  \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}} is a specialized method to
   1.271    solve goals regarding the completeness of pattern matching, as
   1.272    required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
   1.273    \cite{isabelle-function}).
   1.274  
   1.275 -  \item [\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R}] introduces a termination
   1.276 +  \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
   1.277    proof using the relation \isa{R}.  The resulting proof state will
   1.278    contain goals expressing that \isa{R} is wellfounded, and that the
   1.279    arguments of recursive calls decrease with respect to \isa{R}.
   1.280    Usually, this method is used as the initial proof step of manual
   1.281    termination proofs.
   1.282  
   1.283 -  \item [\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
   1.284 +  \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}} attempts a fully
   1.285    automated termination proof by searching for a lexicographic
   1.286    combination of size measures on the arguments of the function. The
   1.287    method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
   1.288 @@ -552,7 +551,7 @@
   1.289    In case of failure, extensive information is printed, which can help
   1.290    to analyse the situation (cf.\ \cite{isabelle-function}).
   1.291  
   1.292 -  \end{descr}%
   1.293 +  \end{description}%
   1.294  \end{isamarkuptext}%
   1.295  \isamarkuptrue%
   1.296  %
   1.297 @@ -564,8 +563,8 @@
   1.298  The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead.
   1.299  
   1.300    \begin{matharray}{rcl}
   1.301 -    \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isartrans{theory}{theory} \\
   1.302 -    \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
   1.303 +    \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isacharparenright}{\isachardoublequote}} \\
   1.304 +    \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   1.305    \end{matharray}
   1.306  
   1.307    \begin{rail}
   1.308 @@ -581,9 +580,9 @@
   1.309      ;
   1.310    \end{rail}
   1.311  
   1.312 -  \begin{descr}
   1.313 +  \begin{description}
   1.314    
   1.315 -  \item [\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}] defines general well-founded
   1.316 +  \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
   1.317    recursive functions (using the TFL package), see also
   1.318    \cite{isabelle-HOL}.  The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells
   1.319    TFL to recover from failed proof attempts, returning unfinished
   1.320 @@ -593,7 +592,7 @@
   1.321    context of the Simplifier (cf.\ \secref{sec:simplifier}) and
   1.322    Classical reasoner (cf.\ \secref{sec:classical}).
   1.323    
   1.324 -  \item [\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
   1.325 +  \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} recommences the
   1.326    proof for leftover termination condition number \isa{i} (default
   1.327    1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
   1.328    constant \isa{c}.
   1.329 @@ -601,15 +600,15 @@
   1.330    Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
   1.331    its internal proofs without manual intervention.
   1.332  
   1.333 -  \end{descr}
   1.334 +  \end{description}
   1.335  
   1.336    \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
   1.337    globally, using the following attributes.
   1.338  
   1.339    \begin{matharray}{rcl}
   1.340 -    \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
   1.341 -    \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
   1.342 -    \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
   1.343 +    \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isa{attribute} \\
   1.344 +    \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isa{attribute} \\
   1.345 +    \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isa{attribute} \\
   1.346    \end{matharray}
   1.347  
   1.348    \begin{rail}
   1.349 @@ -647,11 +646,11 @@
   1.350    to use inference rules for type-checking.
   1.351  
   1.352    \begin{matharray}{rcl}
   1.353 -    \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.354 -    \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.355 -    \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.356 -    \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.357 -    \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isaratt \\
   1.358 +    \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.359 +    \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.360 +    \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.361 +    \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.362 +    \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
   1.363    \end{matharray}
   1.364  
   1.365    \begin{rail}
   1.366 @@ -664,9 +663,9 @@
   1.367      ;
   1.368    \end{rail}
   1.369  
   1.370 -  \begin{descr}
   1.371 +  \begin{description}
   1.372  
   1.373 -  \item [\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}] define (co)inductive predicates from the
   1.374 +  \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the
   1.375    introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part.  The
   1.376    optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
   1.377    (co)inductive predicates that remain fixed throughout the
   1.378 @@ -676,13 +675,13 @@
   1.379    \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
   1.380    for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
   1.381  
   1.382 -  \item [\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}] are wrappers for to the previous commands,
   1.383 +  \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}} are wrappers for to the previous commands,
   1.384    allowing the definition of (co)inductive sets.
   1.385  
   1.386 -  \item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules.  These
   1.387 +  \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules.  These
   1.388    rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
   1.389  
   1.390 -  \end{descr}%
   1.391 +  \end{description}%
   1.392  \end{isamarkuptext}%
   1.393  \isamarkuptrue%
   1.394  %
   1.395 @@ -696,14 +695,14 @@
   1.396  
   1.397    \begin{description}
   1.398  
   1.399 -  \item [\isa{R{\isachardot}intros}] is the list of introduction rules as proven
   1.400 +  \item \isa{R{\isachardot}intros} is the list of introduction rules as proven
   1.401    theorems, for the recursive predicates (or sets).  The rules are
   1.402    also available individually, using the names given them in the
   1.403    theory file;
   1.404  
   1.405 -  \item [\isa{R{\isachardot}cases}] is the case analysis (or elimination) rule;
   1.406 +  \item \isa{R{\isachardot}cases} is the case analysis (or elimination) rule;
   1.407  
   1.408 -  \item [\isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct}] is the (co)induction
   1.409 +  \item \isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct} is the (co)induction
   1.410    rule.
   1.411  
   1.412    \end{description}
   1.413 @@ -766,8 +765,8 @@
   1.414  %
   1.415  \begin{isamarkuptext}%
   1.416  \begin{matharray}{rcl}
   1.417 -    \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isarmeth \\
   1.418 -    \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
   1.419 +    \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
   1.420 +    \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isa{attribute} \\
   1.421    \end{matharray}
   1.422  
   1.423    The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
   1.424 @@ -811,11 +810,11 @@
   1.425    search over and over again.
   1.426  
   1.427    \begin{matharray}{rcl}
   1.428 -    \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   1.429 -    \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.430 -    \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   1.431 -    \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
   1.432 -    \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\
   1.433 +    \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.434 +    \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.435 +    \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.436 +    \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.437 +    \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
   1.438    \end{matharray}
   1.439  
   1.440    \begin{rail}
   1.441 @@ -826,12 +825,12 @@
   1.442    ;
   1.443    \end{rail}
   1.444  
   1.445 -  \begin{descr}
   1.446 +  \begin{description}
   1.447  
   1.448 -  \item [\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}] invokes the specified automated theorem provers on
   1.449 -  the first subgoal.  Provers are run in parallel, the first
   1.450 -  successful result is displayed, and the other attempts are
   1.451 -  terminated.
   1.452 +  \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}
   1.453 +  invokes the specified automated theorem provers on the first
   1.454 +  subgoal.  Provers are run in parallel, the first successful result
   1.455 +  is displayed, and the other attempts are terminated.
   1.456  
   1.457    Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}.  If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as
   1.458    ``ATP provers'' preference by the user interface.
   1.459 @@ -840,32 +839,32 @@
   1.460    and the maximum number of independent prover processes (default: 5);
   1.461    excessive provers are automatically terminated.
   1.462  
   1.463 -  \item [\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated
   1.464 +  \item \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}} prints the list of automated
   1.465    theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}
   1.466    command.
   1.467  
   1.468 -  \item [\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently
   1.469 +  \item \hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}} prints information about presently
   1.470    running provers, including elapsed runtime, and the remaining time
   1.471    until timeout.
   1.472  
   1.473 -  \item [\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running
   1.474 +  \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
   1.475    provers.
   1.476  
   1.477 -  \item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis
   1.478 -  prover with the given facts.  Metis is an automated proof tool of
   1.479 -  medium strength, but is fully integrated into Isabelle/HOL, with
   1.480 -  explicit inferences going through the kernel.  Thus its results are
   1.481 +  \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
   1.482 +  with the given facts.  Metis is an automated proof tool of medium
   1.483 +  strength, but is fully integrated into Isabelle/HOL, with explicit
   1.484 +  inferences going through the kernel.  Thus its results are
   1.485    guaranteed to be ``correct by construction''.
   1.486  
   1.487    Note that all facts used with Metis need to be specified as explicit
   1.488    arguments.  There are no rule declarations as for other Isabelle
   1.489    provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.
   1.490  
   1.491 -  \end{descr}%
   1.492 +  \end{description}%
   1.493  \end{isamarkuptext}%
   1.494  \isamarkuptrue%
   1.495  %
   1.496 -\isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}%
   1.497 +\isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
   1.498  }
   1.499  \isamarkuptrue%
   1.500  %
   1.501 @@ -875,10 +874,10 @@
   1.502    \secref{sec:cases-induct} for proper Isar versions of similar ideas.
   1.503  
   1.504    \begin{matharray}{rcl}
   1.505 -    \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   1.506 -    \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   1.507 -    \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   1.508 -    \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{theory} \\
   1.509 +    \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   1.510 +    \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   1.511 +    \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   1.512 +    \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   1.513    \end{matharray}
   1.514  
   1.515    \begin{rail}
   1.516 @@ -895,11 +894,12 @@
   1.517      ;
   1.518    \end{rail}
   1.519  
   1.520 -  \begin{descr}
   1.521 +  \begin{description}
   1.522  
   1.523 -  \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
   1.524 -  admit to reason about inductive types.  Rules are selected according
   1.525 -  to the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}} attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
   1.526 +  \item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} admit
   1.527 +  to reason about inductive types.  Rules are selected according to
   1.528 +  the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}}
   1.529 +  attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
   1.530  
   1.531    These unstructured tactics feature both goal addressing and dynamic
   1.532    instantiation.  Note that named rule cases are \emph{not} provided
   1.533 @@ -908,7 +908,7 @@
   1.534    statements, only the compact object-logic conclusion of the subgoal
   1.535    being addressed.
   1.536    
   1.537 -  \item [\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}] provide an interface to the internal \verb|mk_cases| operation.  Rules are simplified in an unrestricted
   1.538 +  \item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provide an interface to the internal \verb|mk_cases| operation.  Rules are simplified in an unrestricted
   1.539    forward manner.
   1.540  
   1.541    While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
   1.542 @@ -916,7 +916,7 @@
   1.543    for later use.  The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should
   1.544    be generalized before applying the resulting rule.
   1.545  
   1.546 -  \end{descr}%
   1.547 +  \end{description}%
   1.548  \end{isamarkuptext}%
   1.549  \isamarkuptrue%
   1.550  %
   1.551 @@ -935,12 +935,12 @@
   1.552    (this actually covers the new-style theory format as well).
   1.553  
   1.554    \begin{matharray}{rcl}
   1.555 -    \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.556 -    \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isartrans{theory}{theory} \\
   1.557 -    \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isartrans{theory}{theory} \\
   1.558 -    \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\
   1.559 -    \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\  
   1.560 -    \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
   1.561 +    \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.562 +    \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.563 +    \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.564 +    \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.565 +    \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\  
   1.566 +    \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
   1.567    \end{matharray}
   1.568  
   1.569    \begin{rail}
   1.570 @@ -980,12 +980,12 @@
   1.571    ;
   1.572    \end{rail}
   1.573  
   1.574 -  \begin{descr}
   1.575 +  \begin{description}
   1.576  
   1.577 -  \item [\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t}] evaluates and prints a
   1.578 -  term using the code generator.
   1.579 +  \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a term
   1.580 +  using the code generator.
   1.581  
   1.582 -  \end{descr}
   1.583 +  \end{description}
   1.584  
   1.585    \medskip The other framework generates code from functional programs
   1.586    (including overloading using type classes) to SML \cite{SML}, OCaml
   1.587 @@ -997,21 +997,21 @@
   1.588    introduction on how to use it.
   1.589  
   1.590    \begin{matharray}{rcl}
   1.591 -    \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.592 -    \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.593 -    \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   1.594 -    \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
   1.595 -    \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isartrans{theory}{theory} \\
   1.596 -    \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isartrans{theory}{theory} \\
   1.597 -    \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isartrans{theory}{theory} \\
   1.598 -    \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isartrans{theory}{theory} \\
   1.599 -    \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isartrans{theory}{theory} \\
   1.600 -    \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.601 -    \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.602 -    \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.603 -    \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.604 -    \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.605 -    \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
   1.606 +    \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.607 +    \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.608 +    \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.609 +    \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.610 +    \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.611 +    \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.612 +    \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.613 +    \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.614 +    \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.615 +    \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.616 +    \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.617 +    \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.618 +    \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   1.619 +    \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}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   1.620 +    \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
   1.621    \end{matharray}
   1.622  
   1.623    \begin{rail}
   1.624 @@ -1082,14 +1082,14 @@
   1.625      ;
   1.626    \end{rail}
   1.627  
   1.628 -  \begin{descr}
   1.629 +  \begin{description}
   1.630  
   1.631 -  \item [\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
   1.632 -  for generating and serializing code: for a given list of constants,
   1.633 -  code is generated for the specified target languages.  Abstract code
   1.634 -  is cached incrementally.  If no constant is given, the currently
   1.635 -  cached code is serialized.  If no serialization instruction is
   1.636 -  given, only abstract code is cached.
   1.637 +  \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} is the canonical interface for
   1.638 +  generating and serializing code: for a given list of constants, code
   1.639 +  is generated for the specified target languages.  Abstract code is
   1.640 +  cached incrementally.  If no constant is given, the currently cached
   1.641 +  code is serialized.  If no serialization instruction is given, only
   1.642 +  abstract code is cached.
   1.643  
   1.644    Constants may be specified by giving them literally, referring to
   1.645    all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
   1.646 @@ -1111,71 +1111,70 @@
   1.647    \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
   1.648    declaration.
   1.649  
   1.650 -  \item [\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
   1.651 +  \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
   1.652    representing the corresponding program containing all given
   1.653    constants; if no constants are given, the currently cached code
   1.654    theorems are printed.
   1.655  
   1.656 -  \item [\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
   1.657 +  \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
   1.658    theorems representing the corresponding program containing all given
   1.659    constants; if no constants are given, the currently cached code
   1.660    theorems are visualized.
   1.661  
   1.662 -  \item [\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
   1.663 +  \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
   1.664    for a logical type.
   1.665  
   1.666 -  \item [\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
   1.667 +  \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
   1.668    with target-specific serializations; omitting a serialization
   1.669    deletes an existing serialization.
   1.670  
   1.671 -  \item [\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
   1.672 +  \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
   1.673    constructors with target-specific serializations; omitting a
   1.674    serialization deletes an existing serialization.
   1.675  
   1.676 -  \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
   1.677 -  with target-specific class names; omitting a
   1.678 -  serialization deletes an existing serialization.
   1.679 -  This applies only to \emph{Haskell}.
   1.680 +  \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
   1.681 +  with target-specific class names; omitting a serialization deletes
   1.682 +  an existing serialization.  This applies only to \emph{Haskell}.
   1.683  
   1.684 -  \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
   1.685 +  \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
   1.686    constructor / class instance relations as ``already present'' for a
   1.687    given target.  Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
   1.688    ``already present'' declaration.  This applies only to
   1.689    \emph{Haskell}.
   1.690  
   1.691 -  \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
   1.692 -  mechanism to generate monadic code for Haskell.
   1.693 +  \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
   1.694 +  to generate monadic code for Haskell.
   1.695  
   1.696 -  \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
   1.697 +  \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
   1.698    reserved for a given target, preventing it to be shadowed by any
   1.699    generated code.
   1.700  
   1.701 -  \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
   1.702 +  \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
   1.703    (``include'') to generated code.  A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
   1.704    will remove an already added ``include''.
   1.705  
   1.706 -  \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
   1.707 -  one module name onto another.
   1.708 +  \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
   1.709 +  module name onto another.
   1.710  
   1.711 -  \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which
   1.712 -  are not required to have a definition by means of defining equations;
   1.713 -  if needed these are implemented by program abort instead.
   1.714 +  \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
   1.715 +  required to have a definition by means of defining equations; if
   1.716 +  needed these are implemented by program abort instead.
   1.717  
   1.718 -  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
   1.719 -  with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
   1.720 -  code generation.  Usually packages introducing defining equations
   1.721 -  provide a reasonable default setup for selection.
   1.722 +  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
   1.723 +  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for code
   1.724 +  generation.  Usually packages introducing defining equations provide
   1.725 +  a reasonable default setup for selection.
   1.726  
   1.727 -  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
   1.728 +  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
   1.729    option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
   1.730    applied as rewrite rules to any defining equation during
   1.731    preprocessing.
   1.732  
   1.733 -  \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
   1.734 +  \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
   1.735    selected defining equations, code generator datatypes and
   1.736    preprocessor setup.
   1.737  
   1.738 -  \end{descr}%
   1.739 +  \end{description}%
   1.740  \end{isamarkuptext}%
   1.741  \isamarkuptrue%
   1.742  %
   1.743 @@ -1185,8 +1184,8 @@
   1.744  %
   1.745  \begin{isamarkuptext}%
   1.746  \begin{matharray}{rcl}
   1.747 -    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
   1.748 -    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
   1.749 +    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   1.750 +    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   1.751    \end{matharray}
   1.752  
   1.753    \begin{rail}
   1.754 @@ -1195,27 +1194,27 @@
   1.755    decl: ((name ':')? term '(' 'overloaded' ')'?)
   1.756    \end{rail}
   1.757  
   1.758 -  \begin{descr}
   1.759 +  \begin{description}
   1.760  
   1.761 -  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
   1.762 +  \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up a
   1.763    goal stating the existence of terms with the properties specified to
   1.764    hold for the constants given in \isa{decls}.  After finishing the
   1.765    proof, the theory will be augmented with definitions for the given
   1.766    constants, as well as with theorems stating the properties for these
   1.767    constants.
   1.768  
   1.769 -  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
   1.770 -  up a goal stating the existence of terms with the properties
   1.771 -  specified to hold for the constants given in \isa{decls}.  After
   1.772 -  finishing the proof, the theory will be augmented with axioms
   1.773 -  expressing the properties given in the first place.
   1.774 +  \item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up
   1.775 +  a goal stating the existence of terms with the properties specified
   1.776 +  to hold for the constants given in \isa{decls}.  After finishing
   1.777 +  the proof, the theory will be augmented with axioms expressing the
   1.778 +  properties given in the first place.
   1.779  
   1.780 -  \item [\isa{decl}] declares a constant to be defined by the
   1.781 +  \item \isa{decl} declares a constant to be defined by the
   1.782    specification given.  The definition for the constant \isa{c} is
   1.783    bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
   1.784    the declaration.  Overloaded constants should be declared as such.
   1.785  
   1.786 -  \end{descr}
   1.787 +  \end{description}
   1.788  
   1.789    Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
   1.790    construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the