doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 26907 75466ad27dd7
parent 26902 8db1e960d636
child 26987 978cefd606ad
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 15 18:12:24 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 15 18:12:43 2008 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{matharray}{rcl}
     1.7 -    \hyperlink{attribute.HOL.split_format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
     1.8 +    \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12 @@ -105,7 +105,7 @@
    1.13  
    1.14    \begin{descr}
    1.15    
    1.16 -  \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.17 +  \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.18    low-level tuple types into canonical form as specified by the
    1.19    arguments given; the \isa{i}-th collection of arguments refers to
    1.20    occurrences in premise \isa{i} of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function
    1.21 @@ -365,7 +365,7 @@
    1.22  \begin{isamarkuptext}%
    1.23  \begin{matharray}{rcl}
    1.24      \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
    1.25 -    \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep_datatype}{\hyperlink{command.HOL.rep_datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
    1.26 +    \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
    1.27    \end{matharray}
    1.28  
    1.29    \begin{rail}
    1.30 @@ -386,7 +386,7 @@
    1.31    \item [\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}] defines inductive datatypes in
    1.32    HOL.
    1.33  
    1.34 -  \item [\hyperlink{command.HOL.rep_datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
    1.35 +  \item [\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
    1.36    inductive ones, generating the standard infrastructure of derived
    1.37    concepts (primitive recursion etc.).
    1.38  
    1.39 @@ -399,7 +399,7 @@
    1.40    See \cite{isabelle-HOL} for more details on datatypes, but beware of
    1.41    the old-style theory syntax being used there!  Apart from proper
    1.42    proof methods for case-analysis and induction, there are also
    1.43 -  emulations of ML tactics \hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
    1.44 +  emulations of ML tactics \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
    1.45    to refer directly to the internal structure of subgoals (including
    1.46    internally bound parameters).%
    1.47  \end{isamarkuptext}%
    1.48 @@ -518,9 +518,9 @@
    1.49  %
    1.50  \begin{isamarkuptext}%
    1.51  \begin{matharray}{rcl}
    1.52 -    \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat_completeness}{\hyperlink{method.HOL.pat_completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
    1.53 +    \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
    1.54      \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\
    1.55 -    \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic_order}{\hyperlink{method.HOL.lexicographic_order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
    1.56 +    \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
    1.57    \end{matharray}
    1.58  
    1.59    \begin{rail}
    1.60 @@ -532,7 +532,7 @@
    1.61  
    1.62    \begin{descr}
    1.63  
    1.64 -  \item [\hyperlink{method.HOL.pat_completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
    1.65 +  \item [\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
    1.66    solve goals regarding the completeness of pattern matching, as
    1.67    required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
    1.68    \cite{isabelle-function}).
    1.69 @@ -544,7 +544,7 @@
    1.70    Usually, this method is used as the initial proof step of manual
    1.71    termination proofs.
    1.72  
    1.73 -  \item [\hyperlink{method.HOL.lexicographic_order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
    1.74 +  \item [\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
    1.75    automated termination proof by searching for a lexicographic
    1.76    combination of size measures on the arguments of the function. The
    1.77    method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
    1.78 @@ -564,11 +564,11 @@
    1.79  \isamarkuptrue%
    1.80  %
    1.81  \begin{isamarkuptext}%
    1.82 -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.83 +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.84  
    1.85    \begin{matharray}{rcl}
    1.86      \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isartrans{theory}{theory} \\
    1.87 -    \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.88 +    \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.89    \end{matharray}
    1.90  
    1.91    \begin{rail}
    1.92 @@ -596,7 +596,7 @@
    1.93    context of the Simplifier (cf.\ \secref{sec:simplifier}) and
    1.94    Classical reasoner (cf.\ \secref{sec:classical}).
    1.95    
    1.96 -  \item [\hyperlink{command.HOL.recdef_tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
    1.97 +  \item [\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
    1.98    proof for leftover termination condition number \isa{i} (default
    1.99    1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
   1.100    constant \isa{c}.
   1.101 @@ -610,9 +610,9 @@
   1.102    globally, using the following attributes.
   1.103  
   1.104    \begin{matharray}{rcl}
   1.105 -    \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef_simp}{\hyperlink{attribute.HOL.recdef_simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
   1.106 -    \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef_cong}{\hyperlink{attribute.HOL.recdef_cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
   1.107 -    \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef_wf}{\hyperlink{attribute.HOL.recdef_wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
   1.108 +    \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
   1.109 +    \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
   1.110 +    \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
   1.111    \end{matharray}
   1.112  
   1.113    \begin{rail}
   1.114 @@ -629,7 +629,7 @@
   1.115  \begin{isamarkuptext}%
   1.116  \begin{matharray}{rcl}
   1.117      \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
   1.118 -    \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.119 +    \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.120    \end{matharray}
   1.121  
   1.122    \begin{rail}
   1.123 @@ -647,7 +647,7 @@
   1.124    constants, as well as with theorems stating the properties for these
   1.125    constants.
   1.126  
   1.127 -  \item [\hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
   1.128 +  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
   1.129    up a goal stating the existence of terms with the properties
   1.130    specified to hold for the constants given in \isa{decls}.  After
   1.131    finishing the proof, the theory will be augmented with axioms
   1.132 @@ -660,13 +660,13 @@
   1.133  
   1.134    \end{descr}
   1.135  
   1.136 -  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.137 -  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
   1.138 +  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.139 +  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
   1.140    user has explicitly proven it to be safe.  A practical issue must be
   1.141    considered, though: After introducing two constants with the same
   1.142    properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
   1.143    that the two constants are, in fact, equal.  If this might be a
   1.144 -  problem, one should use \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
   1.145 +  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
   1.146  \end{isamarkuptext}%
   1.147  \isamarkuptrue%
   1.148  %
   1.149 @@ -699,9 +699,9 @@
   1.150  
   1.151    \begin{matharray}{rcl}
   1.152      \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.153 -    \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.154 +    \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.155      \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.156 -    \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.157 +    \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.158      \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isaratt \\
   1.159    \end{matharray}
   1.160  
   1.161 @@ -727,7 +727,7 @@
   1.162    \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
   1.163    for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
   1.164  
   1.165 -  \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.166 +  \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.167    allowing the definition of (co)inductive sets.
   1.168  
   1.169    \item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules.  These
   1.170 @@ -818,14 +818,14 @@
   1.171  \begin{isamarkuptext}%
   1.172  \begin{matharray}{rcl}
   1.173      \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isarmeth \\
   1.174 -    \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith_split}{\hyperlink{attribute.HOL.arith_split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
   1.175 +    \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
   1.176    \end{matharray}
   1.177  
   1.178    The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
   1.179    (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
   1.180    facts are inserted into the goal before running the procedure.
   1.181  
   1.182 -  The \hyperlink{attribute.HOL.arith_split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
   1.183 +  The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
   1.184    rules to be expanded before the arithmetic procedure is invoked.
   1.185  
   1.186    Note that a simpler (but faster) version of arithmetic reasoning is
   1.187 @@ -842,10 +842,10 @@
   1.188    ported to Isar.  These should be never used in proper proof texts!
   1.189  
   1.190    \begin{matharray}{rcl}
   1.191 -    \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.192 -    \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.193 -    \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.194 -    \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive_cases}{\hyperlink{command.HOL.inductive_cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
   1.195 +    \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.196 +    \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.197 +    \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.198 +    \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
   1.199    \end{matharray}
   1.200  
   1.201    \begin{rail}
   1.202 @@ -864,20 +864,20 @@
   1.203  
   1.204    \begin{descr}
   1.205  
   1.206 -  \item [\hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
   1.207 +  \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
   1.208    admit to reason about inductive datatypes only (unless an
   1.209 -  alternative rule is given explicitly).  Furthermore, \hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} does a classical case split on booleans; \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} allows only variables to be given as instantiation.
   1.210 +  alternative rule is given explicitly).  Furthermore, \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} does a classical case split on booleans; \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} allows only variables to be given as instantiation.
   1.211    These tactic emulations feature both goal addressing and dynamic
   1.212    instantiation.  Note that named rule cases are \emph{not} provided
   1.213    as would be by the proper \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} proof
   1.214    methods (see \secref{sec:cases-induct}).
   1.215    
   1.216 -  \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.217 +  \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.218    forward manner.
   1.219  
   1.220 -  While \hyperlink{method.HOL.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
   1.221 -  result immediately as elimination rules, \hyperlink{command.HOL.inductive_cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
   1.222 -  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.223 +  While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
   1.224 +  result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
   1.225 +  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.226    be generalized before applying the resulting rule.
   1.227  
   1.228    \end{descr}%
   1.229 @@ -900,10 +900,10 @@
   1.230  
   1.231    \begin{matharray}{rcl}
   1.232      \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.233 -    \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.234 -    \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.235 -    \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.236 -    \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.237 +    \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.238 +    \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.239 +    \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.240 +    \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.241      \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
   1.242    \end{matharray}
   1.243  
   1.244 @@ -961,20 +961,20 @@
   1.245    introduction on how to use it.
   1.246  
   1.247    \begin{matharray}{rcl}
   1.248 -    \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.249 -    \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.250 -    \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.251 -    \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.252 -    \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.253 -    \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.254 -    \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.255 -    \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.256 -    \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.257 -    \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.258 -    \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.259 -    \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.260 -    \indexdef{HOL}{command}{code\_exception}\hypertarget{command.HOL.code_exception}{\hyperlink{command.HOL.code_exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}} & : & \isartrans{theory}{theory} \\
   1.261 -    \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.262 +    \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.263 +    \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.264 +    \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.265 +    \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.266 +    \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.267 +    \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.268 +    \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.269 +    \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.270 +    \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.271 +    \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.272 +    \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.273 +    \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.274 +    \indexdef{HOL}{command}{code\_exception}\hypertarget{command.HOL.code-exception}{\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}} & : & \isartrans{theory}{theory} \\
   1.275 +    \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.276      \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
   1.277    \end{matharray}
   1.278  
   1.279 @@ -1050,7 +1050,7 @@
   1.280  
   1.281    \begin{descr}
   1.282  
   1.283 -  \item [\hyperlink{command.HOL.export_code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
   1.284 +  \item [\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
   1.285    for generating and serializing code: for a given list of constants,
   1.286    code is generated for the specified target languages.  Abstract code
   1.287    is cached incrementally.  If no constant is given, the currently
   1.288 @@ -1063,7 +1063,7 @@
   1.289  
   1.290    By default, for each involved theory one corresponding name space
   1.291    module is generated.  Alternativly, a module name may be specified
   1.292 -  after the \hyperlink{keyword.module_name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
   1.293 +  after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
   1.294    placed in this module.
   1.295  
   1.296    For \emph{SML} and \emph{OCaml}, the file specification refers to a
   1.297 @@ -1077,54 +1077,54 @@
   1.298    \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.299    declaration.
   1.300  
   1.301 -  \item [\hyperlink{command.HOL.code_thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
   1.302 +  \item [\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
   1.303    representing the corresponding program containing all given
   1.304    constants; if no constants are given, the currently cached code
   1.305    theorems are printed.
   1.306  
   1.307 -  \item [\hyperlink{command.HOL.code_deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
   1.308 +  \item [\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
   1.309    theorems representing the corresponding program containing all given
   1.310    constants; if no constants are given, the currently cached code
   1.311    theorems are visualized.
   1.312  
   1.313 -  \item [\hyperlink{command.HOL.code_datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
   1.314 +  \item [\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
   1.315    for a logical type.
   1.316  
   1.317 -  \item [\hyperlink{command.HOL.code_const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
   1.318 +  \item [\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
   1.319    with target-specific serializations; omitting a serialization
   1.320    deletes an existing serialization.
   1.321  
   1.322 -  \item [\hyperlink{command.HOL.code_type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
   1.323 +  \item [\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
   1.324    constructors with target-specific serializations; omitting a
   1.325    serialization deletes an existing serialization.
   1.326  
   1.327 -  \item [\hyperlink{command.HOL.code_class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
   1.328 +  \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
   1.329    with target-specific class names; in addition, constants associated
   1.330    with this class may be given target-specific names used for instance
   1.331    declarations; omitting a serialization deletes an existing
   1.332    serialization.  This applies only to \emph{Haskell}.
   1.333  
   1.334 -  \item [\hyperlink{command.HOL.code_instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
   1.335 +  \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
   1.336    constructor / class instance relations as ``already present'' for a
   1.337    given target.  Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
   1.338    ``already present'' declaration.  This applies only to
   1.339    \emph{Haskell}.
   1.340  
   1.341 -  \item [\hyperlink{command.HOL.code_monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
   1.342 +  \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
   1.343    mechanism to generate monadic code.
   1.344  
   1.345 -  \item [\hyperlink{command.HOL.code_reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
   1.346 +  \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
   1.347    reserved for a given target, preventing it to be shadowed by any
   1.348    generated code.
   1.349  
   1.350 -  \item [\hyperlink{command.HOL.code_include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
   1.351 +  \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
   1.352    (``include'') to generated code.  A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
   1.353    will remove an already added ``include''.
   1.354  
   1.355 -  \item [\hyperlink{command.HOL.code_modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
   1.356 +  \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
   1.357    one module name onto another.
   1.358  
   1.359 -  \item [\hyperlink{command.HOL.code_exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
   1.360 +  \item [\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
   1.361    are not required to have a definition by a defining equations; these
   1.362    are mapped on exceptions instead.
   1.363  
   1.364 @@ -1138,7 +1138,7 @@
   1.365    applied as rewrite rules to any defining equation during
   1.366    preprocessing.
   1.367  
   1.368 -  \item [\hyperlink{command.HOL.print_codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
   1.369 +  \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
   1.370    selected defining equations, code generator datatypes and
   1.371    preprocessor setup.
   1.372