1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Thu May 15 18:12:24 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Thu May 15 18:12:43 2008 +0200
1.3 @@ -38,9 +38,9 @@
1.4 \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.5 \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
1.6 \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.7 - \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print_abbrevs}{\hyperlink{command.print_abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.8 + \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.9 \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.10 - \indexdef{}{command}{no\_notation}\hypertarget{command.no_notation}{\hyperlink{command.no_notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.11 + \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.12 \end{matharray}
1.13
1.14 These specification mechanisms provide a slightly more abstract view
1.15 @@ -107,7 +107,7 @@
1.16 declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
1.17 \secref{sec:syn-trans}.
1.18
1.19 - \item [\hyperlink{command.print_abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
1.20 + \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
1.21 of the current context.
1.22
1.23 \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
1.24 @@ -116,7 +116,7 @@
1.25 (\secref{sec:syn-trans}). Type declaration and internal syntactic
1.26 representation of the given entity is retrieved from the context.
1.27
1.28 - \item [\hyperlink{command.no_notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the
1.29 + \item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the
1.30 present context.
1.31
1.32 \end{descr}
1.33 @@ -256,10 +256,10 @@
1.34 \begin{isamarkuptext}%
1.35 \begin{matharray}{rcl}
1.36 \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
1.37 - \indexdef{}{command}{print\_locale}\hypertarget{command.print_locale}{\hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.38 - \indexdef{}{command}{print\_locales}\hypertarget{command.print_locales}{\hyperlink{command.print_locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.39 - \indexdef{}{method}{intro\_locales}\hypertarget{method.intro_locales}{\hyperlink{method.intro_locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
1.40 - \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold_locales}{\hyperlink{method.unfold_locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
1.41 + \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.42 + \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.43 + \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
1.44 + \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
1.45 \end{matharray}
1.46
1.47 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
1.48 @@ -382,21 +382,21 @@
1.49 constructions. Predicates are also omitted for empty specification
1.50 texts.
1.51
1.52 - \item [\hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
1.53 + \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
1.54 specified locale expression in a flattened form. The notable
1.55 - special case \hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
1.56 + special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
1.57 contents of the named locale, but keep in mind that type-inference
1.58 will normalize type variables according to the usual alphabetical
1.59 order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
1.60 - Use \hyperlink{command.print_locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
1.61 + Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
1.62
1.63 - \item [\hyperlink{command.print_locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
1.64 + \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
1.65 of the current theory.
1.66
1.67 - \item [\hyperlink{method.intro_locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold_locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
1.68 + \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
1.69 repeatedly expand all introduction rules of locale predicates of the
1.70 - theory. While \hyperlink{method.intro_locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
1.71 - assumptions, \hyperlink{method.unfold_locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
1.72 + theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
1.73 + assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
1.74 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
1.75 specifications entailed by the context, both from target and
1.76 \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
1.77 @@ -421,7 +421,7 @@
1.78 \begin{matharray}{rcl}
1.79 \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\
1.80 \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
1.81 - \indexdef{}{command}{print\_interps}\hypertarget{command.print_interps}{\hyperlink{command.print_interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.82 + \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.83 \end{matharray}
1.84
1.85 \indexouternonterm{interp}
1.86 @@ -511,7 +511,7 @@
1.87 interprets \isa{expr} in the proof context and is otherwise
1.88 similar to interpretation in theories.
1.89
1.90 - \item [\hyperlink{command.print_interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
1.91 + \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
1.92 interpretations of a particular locale \isa{loc} that are active
1.93 in the current context, either theory or proof context. The
1.94 exclamation point argument triggers printing of \emph{witness}
1.95 @@ -560,8 +560,8 @@
1.96 \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
1.97 \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
1.98 \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
1.99 - \indexdef{}{command}{print\_classes}\hypertarget{command.print_classes}{\hyperlink{command.print_classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.100 - \indexdef{}{method}{intro\_classes}\hypertarget{method.intro_classes}{\hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
1.101 + \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.102 + \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
1.103 \end{matharray}
1.104
1.105 \begin{rail}
1.106 @@ -595,7 +595,7 @@
1.107 mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
1.108 corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The
1.109 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
1.110 - --- the \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
1.111 + --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
1.112 class membership proofs.
1.113
1.114 \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\
1.115 @@ -609,7 +609,7 @@
1.116 in Isabelle/HOL.
1.117
1.118 \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets
1.119 - up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
1.120 + up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
1.121 the type classes involved. After finishing the proof, the
1.122 background theory will be augmented by the proven type arities.
1.123
1.124 @@ -618,10 +618,10 @@
1.125 contained in class \isa{d}. After finishing the proof, class
1.126 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
1.127
1.128 - \item [\hyperlink{command.print_classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
1.129 + \item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
1.130 theory.
1.131
1.132 - \item [\hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
1.133 + \item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
1.134 introduction rules of this theory. Note that this method usually
1.135 needs not be named explicitly, as it is already included in the
1.136 default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular,
1.137 @@ -690,7 +690,7 @@
1.138 not contain more than one type variable. The class axioms (with
1.139 implicit sort constraints added) are bound to the given names.
1.140 Furthermore a class introduction rule is generated (being bound as
1.141 - \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
1.142 + \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
1.143
1.144 The ``class axioms'' are stored as theorems according to the given
1.145 name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
1.146 @@ -699,7 +699,7 @@
1.147 \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
1.148 \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}]
1.149 setup a goal stating a class relation or type arity. The proof
1.150 - would usually proceed by \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
1.151 + would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
1.152 the characteristic theorems of the type classes involved. After
1.153 finishing the proof, the theory will be augmented by a type
1.154 signature declaration corresponding to the resulting theorem.
1.155 @@ -769,7 +769,7 @@
1.156 ``global'', which may not be changed within a local context.
1.157
1.158 \begin{matharray}{rcll}
1.159 - \indexdef{}{command}{print\_configs}\hypertarget{command.print_configs}{\hyperlink{command.print_configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}} & : & \isarkeep{theory~|~proof} \\
1.160 + \indexdef{}{command}{print\_configs}\hypertarget{command.print-configs}{\hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}} & : & \isarkeep{theory~|~proof} \\
1.161 \end{matharray}
1.162
1.163 \begin{rail}
1.164 @@ -778,7 +778,7 @@
1.165
1.166 \begin{descr}
1.167
1.168 - \item [\hyperlink{command.print_configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}] prints the available
1.169 + \item [\hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}] prints the available
1.170 configuration options, with names, types, and current values.
1.171
1.172 \item [\isa{{\isachardoublequote}name\ {\isacharequal}\ value{\isachardoublequote}}] as an attribute expression modifies
1.173 @@ -860,9 +860,9 @@
1.174 \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isaratt \\
1.175 \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isaratt \\[0.5ex]
1.176 \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isaratt \\
1.177 - \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim_format}{\hyperlink{attribute.Pure.elim_format}{\mbox{\isa{elim{\isacharunderscore}format}}}} & : & \isaratt \\
1.178 + \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim-format}{\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}}} & : & \isaratt \\
1.179 \indexdef{}{attribute}{standard}\hypertarget{attribute.standard}{\hyperlink{attribute.standard}{\mbox{\isa{standard}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
1.180 - \indexdef{}{attribute}{no\_vars}\hypertarget{attribute.no_vars}{\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
1.181 + \indexdef{}{attribute}{no\_vars}\hypertarget{attribute.no-vars}{\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
1.182 \end{matharray}
1.183
1.184 \begin{rail}
1.185 @@ -899,7 +899,7 @@
1.186 \item [\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n}] rotate the premises of a
1.187 theorem by \isa{n} (default 1).
1.188
1.189 - \item [\hyperlink{attribute.Pure.elim_format}{\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}}] turns a destruction rule into
1.190 + \item [\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}}] turns a destruction rule into
1.191 elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
1.192
1.193 Note that the Classical Reasoner (\secref{sec:classical}) provides
1.194 @@ -910,7 +910,7 @@
1.195 operation violates the local proof context (including active
1.196 locales).
1.197
1.198 - \item [\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}}] replaces schematic variables by free
1.199 + \item [\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}}] replaces schematic variables by free
1.200 ones; this is mainly for tuning output of pretty printed theorems.
1.201
1.202 \end{descr}%
1.203 @@ -950,15 +950,15 @@
1.204 \secref{sec:pure-meth-att}).
1.205
1.206 \begin{matharray}{rcl}
1.207 - \indexdef{}{method}{rule\_tac}\hypertarget{method.rule_tac}{\hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.208 - \indexdef{}{method}{erule\_tac}\hypertarget{method.erule_tac}{\hyperlink{method.erule_tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.209 - \indexdef{}{method}{drule\_tac}\hypertarget{method.drule_tac}{\hyperlink{method.drule_tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.210 - \indexdef{}{method}{frule\_tac}\hypertarget{method.frule_tac}{\hyperlink{method.frule_tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.211 - \indexdef{}{method}{cut\_tac}\hypertarget{method.cut_tac}{\hyperlink{method.cut_tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.212 - \indexdef{}{method}{thin\_tac}\hypertarget{method.thin_tac}{\hyperlink{method.thin_tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.213 - \indexdef{}{method}{subgoal\_tac}\hypertarget{method.subgoal_tac}{\hyperlink{method.subgoal_tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.214 - \indexdef{}{method}{rename\_tac}\hypertarget{method.rename_tac}{\hyperlink{method.rename_tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.215 - \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate_tac}{\hyperlink{method.rotate_tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.216 + \indexdef{}{method}{rule\_tac}\hypertarget{method.rule-tac}{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.217 + \indexdef{}{method}{erule\_tac}\hypertarget{method.erule-tac}{\hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.218 + \indexdef{}{method}{drule\_tac}\hypertarget{method.drule-tac}{\hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.219 + \indexdef{}{method}{frule\_tac}\hypertarget{method.frule-tac}{\hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.220 + \indexdef{}{method}{cut\_tac}\hypertarget{method.cut-tac}{\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.221 + \indexdef{}{method}{thin\_tac}\hypertarget{method.thin-tac}{\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.222 + \indexdef{}{method}{subgoal\_tac}\hypertarget{method.subgoal-tac}{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.223 + \indexdef{}{method}{rename\_tac}\hypertarget{method.rename-tac}{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.224 + \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate-tac}{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.225 \indexdef{}{method}{tactic}\hypertarget{method.tactic}{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.226 \end{matharray}
1.227
1.228 @@ -981,31 +981,31 @@
1.229
1.230 \begin{descr}
1.231
1.232 - \item [\hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc.] do resolution of rules with explicit
1.233 + \item [\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc.] do resolution of rules with explicit
1.234 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}).
1.235
1.236 Multiple rules may be only given if there is no instantiation; then
1.237 - \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
1.238 + \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
1.239 \cite[\S3]{isabelle-ref}).
1.240
1.241 - \item [\hyperlink{method.cut_tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}] inserts facts into the proof state as
1.242 + \item [\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}] inserts facts into the proof state as
1.243 assumption of a subgoal, see also \verb|cut_facts_tac| in
1.244 \cite[\S3]{isabelle-ref}. Note that the scope of schematic
1.245 variables is spread over the main goal statement. Instantiations
1.246 may be given as well, see also ML tactic \verb|cut_inst_tac| in
1.247 \cite[\S3]{isabelle-ref}.
1.248
1.249 - \item [\hyperlink{method.thin_tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] deletes the specified
1.250 + \item [\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] deletes the specified
1.251 assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic
1.252 variables. See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
1.253
1.254 - \item [\hyperlink{method.subgoal_tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an
1.255 + \item [\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an
1.256 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
1.257
1.258 - \item [\hyperlink{method.rename_tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames
1.259 + \item [\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames
1.260 parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables.
1.261
1.262 - \item [\hyperlink{method.rotate_tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n}] rotates the assumptions of a
1.263 + \item [\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n}] rotates the assumptions of a
1.264 goal by \isa{n} positions: from right to left if \isa{n} is
1.265 positive, and from left to right if \isa{n} is negative; the
1.266 default value is 1. See also \verb|rotate_tac| in
1.267 @@ -1042,7 +1042,7 @@
1.268 \begin{isamarkuptext}%
1.269 \begin{matharray}{rcl}
1.270 \indexdef{}{method}{simp}\hypertarget{method.simp}{\hyperlink{method.simp}{\mbox{\isa{simp}}}} & : & \isarmeth \\
1.271 - \indexdef{}{method}{simp\_all}\hypertarget{method.simp_all}{\hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}}} & : & \isarmeth \\
1.272 + \indexdef{}{method}{simp\_all}\hypertarget{method.simp-all}{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}} & : & \isarmeth \\
1.273 \end{matharray}
1.274
1.275 \indexouternonterm{simpmod}
1.276 @@ -1075,7 +1075,7 @@
1.277 include the Splitter (all major object logics such HOL, HOLCF, FOL,
1.278 ZF do this already).
1.279
1.280 - \item [\hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}}] is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on
1.281 + \item [\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}] is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on
1.282 all goals (backwards from the last to the first one).
1.283
1.284 \end{descr}
1.285 @@ -1116,7 +1116,7 @@
1.286 %
1.287 \begin{isamarkuptext}%
1.288 \begin{matharray}{rcl}
1.289 - \indexdef{}{command}{print\_simpset}\hypertarget{command.print_simpset}{\hyperlink{command.print_simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.290 + \indexdef{}{command}{print\_simpset}\hypertarget{command.print-simpset}{\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.291 \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isaratt \\
1.292 \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isaratt \\
1.293 \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isaratt \\
1.294 @@ -1129,7 +1129,7 @@
1.295
1.296 \begin{descr}
1.297
1.298 - \item [\hyperlink{command.print_simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}] prints the collection of rules
1.299 + \item [\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}] prints the collection of rules
1.300 declared to the Simplifier, which is also known as ``simpset''
1.301 internally \cite{isabelle-ref}.
1.302
1.303 @@ -1149,7 +1149,7 @@
1.304 %
1.305 \begin{isamarkuptext}%
1.306 \begin{matharray}{rcl}
1.307 - \indexdef{}{command}{simproc\_setup}\hypertarget{command.simproc_setup}{\hyperlink{command.simproc_setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.308 + \indexdef{}{command}{simproc\_setup}\hypertarget{command.simproc-setup}{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.309 simproc & : & \isaratt \\
1.310 \end{matharray}
1.311
1.312 @@ -1163,7 +1163,7 @@
1.313
1.314 \begin{descr}
1.315
1.316 - \item [\hyperlink{command.simproc_setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}] defines a named simplification
1.317 + \item [\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}] defines a named simplification
1.318 procedure that is invoked by the Simplifier whenever any of the
1.319 given term patterns match the current redex. The implementation,
1.320 which is provided as ML source text, needs to be of type \verb|"morphism -> simpset -> cterm -> thm option"|, where the \verb|cterm| represents the current redex \isa{r} and the result is
1.321 @@ -1182,7 +1182,7 @@
1.322
1.323 \item [\isa{{\isachardoublequote}simproc\ add{\isacharcolon}\ name{\isachardoublequote}} and \isa{{\isachardoublequote}simproc\ del{\isacharcolon}\ name{\isachardoublequote}}]
1.324 add or delete named simprocs to the current Simplifier context. The
1.325 - default is to add a simproc. Note that \hyperlink{command.simproc_setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}
1.326 + default is to add a simproc. Note that \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}
1.327 already adds the new simproc to the subsequent context.
1.328
1.329 \end{descr}%
1.330 @@ -1436,7 +1436,7 @@
1.331 %
1.332 \begin{isamarkuptext}%
1.333 \begin{matharray}{rcl}
1.334 - \indexdef{}{command}{print\_claset}\hypertarget{command.print_claset}{\hyperlink{command.print_claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.335 + \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.336 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isaratt \\
1.337 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isaratt \\
1.338 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isaratt \\
1.339 @@ -1455,7 +1455,7 @@
1.340
1.341 \begin{descr}
1.342
1.343 - \item [\hyperlink{command.print_claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}] prints the collection of rules
1.344 + \item [\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}] prints the collection of rules
1.345 declared to the Classical Reasoner, which is also known as
1.346 ``claset'' internally \cite{isabelle-ref}.
1.347
1.348 @@ -1515,9 +1515,9 @@
1.349 \begin{isamarkuptext}%
1.350 \begin{matharray}{rcl}
1.351 \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
1.352 - \indexdef{}{command}{print\_cases}\hypertarget{command.print_cases}{\hyperlink{command.print_cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
1.353 - \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case_names}{\hyperlink{attribute.case_names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\
1.354 - \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case_conclusion}{\hyperlink{attribute.case_conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\
1.355 + \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
1.356 + \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\
1.357 + \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\
1.358 \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isaratt \\
1.359 \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isaratt \\
1.360 \end{matharray}
1.361 @@ -1585,15 +1585,15 @@
1.362 proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).
1.363 The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.
1.364
1.365 - \item [\hyperlink{command.print_cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the
1.366 + \item [\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the
1.367 current state, using Isar proof language notation.
1.368
1.369 - \item [\hyperlink{attribute.case_names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}]
1.370 + \item [\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}]
1.371 declares names for the local contexts of premises of a theorem;
1.372 \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the
1.373 list of premises.
1.374
1.375 - \item [\hyperlink{attribute.case_conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise
1.376 + \item [\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise
1.377 \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the
1.378 prefix of arguments of a logical formula built by nesting a binary
1.379 connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
1.380 @@ -1775,7 +1775,7 @@
1.381 the conclusion will be provided with each case, provided that term
1.382 is fully specified.
1.383
1.384 - The \hyperlink{command.print_cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
1.385 + The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
1.386 in the current proof state.
1.387
1.388 \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
1.389 @@ -1815,7 +1815,7 @@
1.390 %
1.391 \begin{isamarkuptext}%
1.392 \begin{matharray}{rcl}
1.393 - \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print_induct_rules}{\hyperlink{command.print_induct_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.394 + \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.395 \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isaratt \\
1.396 \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isaratt \\
1.397 \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isaratt \\
1.398 @@ -1835,7 +1835,7 @@
1.399
1.400 \begin{descr}
1.401
1.402 - \item [\hyperlink{command.print_induct_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct
1.403 + \item [\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct
1.404 rules for predicates (or sets) and types of the current context.
1.405
1.406 \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}] (as attributes) augment the corresponding context of
1.407 @@ -1845,7 +1845,7 @@
1.408 cases and induction rules as expected, so users rarely need to
1.409 intervene.
1.410
1.411 - Manual rule declarations usually refer to the \hyperlink{attribute.case_names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
1.412 + Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
1.413 cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
1.414 declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
1.415
1.416 @@ -1862,7 +1862,7 @@
1.417 \indexdef{}{command}{judgment}\hypertarget{command.judgment}{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}} & : & \isartrans{theory}{theory} \\
1.418 \indexdef{}{method}{atomize}\hypertarget{method.atomize}{\hyperlink{method.atomize}{\mbox{\isa{atomize}}}} & : & \isarmeth \\
1.419 \indexdef{}{attribute}{atomize}\hypertarget{attribute.atomize}{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}} & : & \isaratt \\
1.420 - \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule_format}{\hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}}} & : & \isaratt \\
1.421 + \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule-format}{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}}} & : & \isaratt \\
1.422 \indexdef{}{attribute}{rulify}\hypertarget{attribute.rulify}{\hyperlink{attribute.rulify}{\mbox{\isa{rulify}}}} & : & \isaratt \\
1.423 \end{matharray}
1.424
1.425 @@ -1878,7 +1878,7 @@
1.426 e.g.\ \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}} versus \isa{{\isachardoublequote}{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x{\isachardoublequote}}.
1.427
1.428 From the following language elements, only the \hyperlink{method.atomize}{\mbox{\isa{atomize}}}
1.429 - method and \hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}} attribute are occasionally
1.430 + method and \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} attribute are occasionally
1.431 required by end-users, the rest is for those who need to setup their
1.432 own object-logic. In the latter case existing formulations of
1.433 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
1.434 @@ -1919,13 +1919,13 @@
1.435 Meta-level conjunction should be covered as well (this is
1.436 particularly important for locales, see \secref{sec:locale}).
1.437
1.438 - \item [\hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}}] rewrites a theorem by the
1.439 + \item [\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}}] rewrites a theorem by the
1.440 equalities declared as \hyperlink{attribute.rulify}{\mbox{\isa{rulify}}} rules in the current
1.441 object-logic. By default, the result is fully normalized, including
1.442 assumptions and conclusions at any depth. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}}
1.443 option restricts the transformation to the conclusion of a rule.
1.444
1.445 - In common object-logics (HOL, FOL, ZF), the effect of \hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}} is to replace (bounded) universal quantification
1.446 + In common object-logics (HOL, FOL, ZF), the effect of \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} is to replace (bounded) universal quantification
1.447 (\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}) and implication (\isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}}) by the corresponding
1.448 rule statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}.
1.449
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 15 18:12:24 2008 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 15 18:12:43 2008 +0200
2.3 @@ -95,7 +95,7 @@
2.4 %
2.5 \begin{isamarkuptext}%
2.6 \begin{matharray}{rcl}
2.7 - \hyperlink{attribute.HOL.split_format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
2.8 + \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
2.9 \end{matharray}
2.10
2.11 \begin{rail}
2.12 @@ -105,7 +105,7 @@
2.13
2.14 \begin{descr}
2.15
2.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
2.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
2.18 low-level tuple types into canonical form as specified by the
2.19 arguments given; the \isa{i}-th collection of arguments refers to
2.20 occurrences in premise \isa{i} of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function
2.21 @@ -365,7 +365,7 @@
2.22 \begin{isamarkuptext}%
2.23 \begin{matharray}{rcl}
2.24 \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
2.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} \\
2.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} \\
2.27 \end{matharray}
2.28
2.29 \begin{rail}
2.30 @@ -386,7 +386,7 @@
2.31 \item [\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}] defines inductive datatypes in
2.32 HOL.
2.33
2.34 - \item [\hyperlink{command.HOL.rep_datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
2.35 + \item [\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
2.36 inductive ones, generating the standard infrastructure of derived
2.37 concepts (primitive recursion etc.).
2.38
2.39 @@ -399,7 +399,7 @@
2.40 See \cite{isabelle-HOL} for more details on datatypes, but beware of
2.41 the old-style theory syntax being used there! Apart from proper
2.42 proof methods for case-analysis and induction, there are also
2.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
2.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
2.45 to refer directly to the internal structure of subgoals (including
2.46 internally bound parameters).%
2.47 \end{isamarkuptext}%
2.48 @@ -518,9 +518,9 @@
2.49 %
2.50 \begin{isamarkuptext}%
2.51 \begin{matharray}{rcl}
2.52 - \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat_completeness}{\hyperlink{method.HOL.pat_completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
2.53 + \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
2.54 \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\
2.55 - \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic_order}{\hyperlink{method.HOL.lexicographic_order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
2.56 + \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
2.57 \end{matharray}
2.58
2.59 \begin{rail}
2.60 @@ -532,7 +532,7 @@
2.61
2.62 \begin{descr}
2.63
2.64 - \item [\hyperlink{method.HOL.pat_completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
2.65 + \item [\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
2.66 solve goals regarding the completeness of pattern matching, as
2.67 required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
2.68 \cite{isabelle-function}).
2.69 @@ -544,7 +544,7 @@
2.70 Usually, this method is used as the initial proof step of manual
2.71 termination proofs.
2.72
2.73 - \item [\hyperlink{method.HOL.lexicographic_order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
2.74 + \item [\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
2.75 automated termination proof by searching for a lexicographic
2.76 combination of size measures on the arguments of the function. The
2.77 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
2.78 @@ -564,11 +564,11 @@
2.79 \isamarkuptrue%
2.80 %
2.81 \begin{isamarkuptext}%
2.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.
2.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.
2.84
2.85 \begin{matharray}{rcl}
2.86 \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isartrans{theory}{theory} \\
2.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)} \\
2.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)} \\
2.89 \end{matharray}
2.90
2.91 \begin{rail}
2.92 @@ -596,7 +596,7 @@
2.93 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
2.94 Classical reasoner (cf.\ \secref{sec:classical}).
2.95
2.96 - \item [\hyperlink{command.HOL.recdef_tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
2.97 + \item [\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
2.98 proof for leftover termination condition number \isa{i} (default
2.99 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
2.100 constant \isa{c}.
2.101 @@ -610,9 +610,9 @@
2.102 globally, using the following attributes.
2.103
2.104 \begin{matharray}{rcl}
2.105 - \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef_simp}{\hyperlink{attribute.HOL.recdef_simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
2.106 - \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef_cong}{\hyperlink{attribute.HOL.recdef_cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
2.107 - \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef_wf}{\hyperlink{attribute.HOL.recdef_wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
2.108 + \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
2.109 + \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
2.110 + \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
2.111 \end{matharray}
2.112
2.113 \begin{rail}
2.114 @@ -629,7 +629,7 @@
2.115 \begin{isamarkuptext}%
2.116 \begin{matharray}{rcl}
2.117 \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
2.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)} \\
2.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)} \\
2.120 \end{matharray}
2.121
2.122 \begin{rail}
2.123 @@ -647,7 +647,7 @@
2.124 constants, as well as with theorems stating the properties for these
2.125 constants.
2.126
2.127 - \item [\hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
2.128 + \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
2.129 up a goal stating the existence of terms with the properties
2.130 specified to hold for the constants given in \isa{decls}. After
2.131 finishing the proof, the theory will be augmented with axioms
2.132 @@ -660,13 +660,13 @@
2.133
2.134 \end{descr}
2.135
2.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
2.137 - construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
2.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
2.139 + construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
2.140 user has explicitly proven it to be safe. A practical issue must be
2.141 considered, though: After introducing two constants with the same
2.142 properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
2.143 that the two constants are, in fact, equal. If this might be a
2.144 - problem, one should use \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
2.145 + problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
2.146 \end{isamarkuptext}%
2.147 \isamarkuptrue%
2.148 %
2.149 @@ -699,9 +699,9 @@
2.150
2.151 \begin{matharray}{rcl}
2.152 \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
2.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} \\
2.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} \\
2.155 \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
2.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} \\
2.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} \\
2.158 \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isaratt \\
2.159 \end{matharray}
2.160
2.161 @@ -727,7 +727,7 @@
2.162 \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
2.163 for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
2.164
2.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,
2.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,
2.167 allowing the definition of (co)inductive sets.
2.168
2.169 \item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules. These
2.170 @@ -818,14 +818,14 @@
2.171 \begin{isamarkuptext}%
2.172 \begin{matharray}{rcl}
2.173 \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isarmeth \\
2.174 - \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith_split}{\hyperlink{attribute.HOL.arith_split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
2.175 + \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
2.176 \end{matharray}
2.177
2.178 The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
2.179 (on types \isa{nat}, \isa{int}, \isa{real}). Any current
2.180 facts are inserted into the goal before running the procedure.
2.181
2.182 - The \hyperlink{attribute.HOL.arith_split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
2.183 + The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
2.184 rules to be expanded before the arithmetic procedure is invoked.
2.185
2.186 Note that a simpler (but faster) version of arithmetic reasoning is
2.187 @@ -842,10 +842,10 @@
2.188 ported to Isar. These should be never used in proper proof texts!
2.189
2.190 \begin{matharray}{rcl}
2.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 \\
2.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 \\
2.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 \\
2.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} \\
2.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 \\
2.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 \\
2.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 \\
2.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} \\
2.199 \end{matharray}
2.200
2.201 \begin{rail}
2.202 @@ -864,20 +864,20 @@
2.203
2.204 \begin{descr}
2.205
2.206 - \item [\hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
2.207 + \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
2.208 admit to reason about inductive datatypes only (unless an
2.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.
2.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.
2.211 These tactic emulations feature both goal addressing and dynamic
2.212 instantiation. Note that named rule cases are \emph{not} provided
2.213 as would be by the proper \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} proof
2.214 methods (see \secref{sec:cases-induct}).
2.215
2.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
2.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
2.218 forward manner.
2.219
2.220 - While \hyperlink{method.HOL.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
2.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
2.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
2.223 + While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
2.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
2.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
2.226 be generalized before applying the resulting rule.
2.227
2.228 \end{descr}%
2.229 @@ -900,10 +900,10 @@
2.230
2.231 \begin{matharray}{rcl}
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.241 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
2.242 \end{matharray}
2.243
2.244 @@ -961,20 +961,20 @@
2.245 introduction on how to use it.
2.246
2.247 \begin{matharray}{rcl}
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.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} \\
2.276 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
2.277 \end{matharray}
2.278
2.279 @@ -1050,7 +1050,7 @@
2.280
2.281 \begin{descr}
2.282
2.283 - \item [\hyperlink{command.HOL.export_code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
2.284 + \item [\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
2.285 for generating and serializing code: for a given list of constants,
2.286 code is generated for the specified target languages. Abstract code
2.287 is cached incrementally. If no constant is given, the currently
2.288 @@ -1063,7 +1063,7 @@
2.289
2.290 By default, for each involved theory one corresponding name space
2.291 module is generated. Alternativly, a module name may be specified
2.292 - after the \hyperlink{keyword.module_name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
2.293 + after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
2.294 placed in this module.
2.295
2.296 For \emph{SML} and \emph{OCaml}, the file specification refers to a
2.297 @@ -1077,54 +1077,54 @@
2.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
2.299 declaration.
2.300
2.301 - \item [\hyperlink{command.HOL.code_thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
2.302 + \item [\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
2.303 representing the corresponding program containing all given
2.304 constants; if no constants are given, the currently cached code
2.305 theorems are printed.
2.306
2.307 - \item [\hyperlink{command.HOL.code_deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
2.308 + \item [\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
2.309 theorems representing the corresponding program containing all given
2.310 constants; if no constants are given, the currently cached code
2.311 theorems are visualized.
2.312
2.313 - \item [\hyperlink{command.HOL.code_datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
2.314 + \item [\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
2.315 for a logical type.
2.316
2.317 - \item [\hyperlink{command.HOL.code_const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
2.318 + \item [\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
2.319 with target-specific serializations; omitting a serialization
2.320 deletes an existing serialization.
2.321
2.322 - \item [\hyperlink{command.HOL.code_type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
2.323 + \item [\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
2.324 constructors with target-specific serializations; omitting a
2.325 serialization deletes an existing serialization.
2.326
2.327 - \item [\hyperlink{command.HOL.code_class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
2.328 + \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
2.329 with target-specific class names; in addition, constants associated
2.330 with this class may be given target-specific names used for instance
2.331 declarations; omitting a serialization deletes an existing
2.332 serialization. This applies only to \emph{Haskell}.
2.333
2.334 - \item [\hyperlink{command.HOL.code_instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
2.335 + \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
2.336 constructor / class instance relations as ``already present'' for a
2.337 given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
2.338 ``already present'' declaration. This applies only to
2.339 \emph{Haskell}.
2.340
2.341 - \item [\hyperlink{command.HOL.code_monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
2.342 + \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
2.343 mechanism to generate monadic code.
2.344
2.345 - \item [\hyperlink{command.HOL.code_reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
2.346 + \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
2.347 reserved for a given target, preventing it to be shadowed by any
2.348 generated code.
2.349
2.350 - \item [\hyperlink{command.HOL.code_include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
2.351 + \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
2.352 (``include'') to generated code. A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
2.353 will remove an already added ``include''.
2.354
2.355 - \item [\hyperlink{command.HOL.code_modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
2.356 + \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
2.357 one module name onto another.
2.358
2.359 - \item [\hyperlink{command.HOL.code_exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
2.360 + \item [\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
2.361 are not required to have a definition by a defining equations; these
2.362 are mapped on exceptions instead.
2.363
2.364 @@ -1138,7 +1138,7 @@
2.365 applied as rewrite rules to any defining equation during
2.366 preprocessing.
2.367
2.368 - \item [\hyperlink{command.HOL.print_codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
2.369 + \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
2.370 selected defining equations, code generator datatypes and
2.371 preprocessor setup.
2.372
3.1 --- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex Thu May 15 18:12:24 2008 +0200
3.2 +++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex Thu May 15 18:12:43 2008 +0200
3.3 @@ -67,8 +67,8 @@
3.4
3.5 \end{enumerate}
3.6
3.7 - Basically, the set of Isar tactic emulations \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}},
3.8 - \hyperlink{method.erule_tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}, \hyperlink{method.drule_tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}, \hyperlink{method.frule_tac}{\mbox{\isa{frule{\isacharunderscore}tac}}} (see
3.9 + Basically, the set of Isar tactic emulations \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}},
3.10 + \hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}, \hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}, \hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}} (see
3.11 \secref{sec:tactics}) would be sufficient to cover the four modes,
3.12 either with or without instantiation, and either with single or
3.13 multiple arguments. Although it is more convenient in most cases to
3.14 @@ -76,7 +76,7 @@
3.15 \secref{sec:pure-meth-att}), or any of its ``improper'' variants
3.16 \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see
3.17 \secref{sec:misc-meth-att}). Note that explicit goal addressing is
3.18 - only supported by the actual \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} version.
3.19 + only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} version.
3.20
3.21 With this in mind, plain resolution tactics correspond to Isar
3.22 methods as follows.
3.23 @@ -106,15 +106,15 @@
3.24 \begin{isamarkuptext}%
3.25 The main Simplifier tactics \verb|simp_tac| and variants (cf.\
3.26 \cite{isabelle-ref}) are all covered by the \hyperlink{method.simp}{\mbox{\isa{simp}}} and
3.27 - \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} methods (see \secref{sec:simplifier}). Note that
3.28 + \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} methods (see \secref{sec:simplifier}). Note that
3.29 there is no individual goal addressing available, simplification
3.30 acts either on the first goal (\hyperlink{method.simp}{\mbox{\isa{simp}}}) or all goals
3.31 - (\hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}}).
3.32 + (\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}).
3.33
3.34 \medskip
3.35 \begin{tabular}{lll}
3.36 \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\
3.37 - \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} \\[0.5ex]
3.38 + \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} \\[0.5ex]
3.39 \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\
3.40 \verb|asm_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} \\
3.41 \verb|full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}} \\
3.42 @@ -193,7 +193,7 @@
3.43 \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see
3.44 \cite{isabelle-ref}) are not available in Isar, since there is no
3.45 direct goal addressing. Nevertheless, some basic methods address
3.46 - all goals internally, notably \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} (see
3.47 + all goals internally, notably \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} (see
3.48 \secref{sec:simplifier}). Also note that \verb|ALLGOALS| can be
3.49 often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although
3.50 this usually has a different operational behavior, such as solving
4.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Thu May 15 18:12:24 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Thu May 15 18:12:43 2008 +0200
4.3 @@ -217,7 +217,7 @@
4.4 of the premises of the rule involved. Note that positions may be
4.5 easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example. This involves the trivial rule
4.6 \isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
4.7 - ``\indexref{}{fact}{\_}\hyperlink{fact._}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
4.8 + ``\indexref{}{fact}{\_}\hyperlink{fact.-}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
4.9
4.10 Automated methods (such as \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.auto}{\mbox{\isa{auto}}}) just
4.11 insert any given facts before their usual operation. Depending on
4.12 @@ -239,7 +239,7 @@
4.13 \indexdef{}{command}{show}\hypertarget{command.show}{\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
4.14 \indexdef{}{command}{hence}\hypertarget{command.hence}{\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}}} & : & \isartrans{proof(state)}{proof(prove)} \\
4.15 \indexdef{}{command}{thus}\hypertarget{command.thus}{\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}} & : & \isartrans{proof(state)}{proof(prove)} \\
4.16 - \indexdef{}{command}{print\_statement}\hypertarget{command.print_statement}{\hyperlink{command.print_statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
4.17 + \indexdef{}{command}{print\_statement}\hypertarget{command.print-statement}{\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
4.18 \end{matharray}
4.19
4.20 From a theory context, proof mode is entered by an initial goal
4.21 @@ -335,7 +335,7 @@
4.22 \item [\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}}] abbreviates ``\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''. Note that \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} is also equivalent to
4.23 ``\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}''.
4.24
4.25 - \item [\hyperlink{command.print_statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}~\isa{a}] prints facts from the
4.26 + \item [\hyperlink{command.print-statement}{\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}}~\isa{a}] prints facts from the
4.27 current theory or proof context in long statement form, according to
4.28 the syntax for \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} given above.
4.29
4.30 @@ -344,7 +344,7 @@
4.31 Any goal statement causes some term abbreviations (such as
4.32 \indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also
4.33 \secref{sec:term-abbrev}. Furthermore, the local context of a
4.34 - (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\hyperlink{case.rule_context}{\mbox{\isa{rule{\isacharunderscore}context}}} case.
4.35 + (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\hyperlink{case.rule-context}{\mbox{\isa{rule{\isacharunderscore}context}}} case.
4.36
4.37 The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold
4.38 meaning: (1) during the of this claim they refer to the the local
4.39 @@ -635,7 +635,7 @@
4.40 goal statements with a list of patterns ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. In both cases, higher-order matching is invoked to
4.41 bind extra-logical term variables, which may be either named
4.42 schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
4.43 - ``\hyperlink{variable._}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
4.44 + ``\hyperlink{variable.-}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
4.45 form the patterns occur on the left-hand side, while the \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns are in postfix position.
4.46
4.47 Polymorphism of term bindings is handled in Hindley-Milner style,
4.48 @@ -746,7 +746,7 @@
4.49
4.50 \begin{matharray}{rcl}
4.51 \indexdef{}{command}{apply}\hypertarget{command.apply}{\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(prove)} \\
4.52 - \indexdef{}{command}{apply\_end}\hypertarget{command.apply_end}{\hyperlink{command.apply_end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(state)} \\
4.53 + \indexdef{}{command}{apply\_end}\hypertarget{command.apply-end}{\hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(state)} \\
4.54 \indexdef{}{command}{done}\hypertarget{command.done}{\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(state)} \\
4.55 \indexdef{}{command}{defer}\hypertarget{command.defer}{\hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
4.56 \indexdef{}{command}{prefer}\hypertarget{command.prefer}{\hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
4.57 @@ -774,7 +774,7 @@
4.58 further \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command would always work in a purely
4.59 backward manner.
4.60
4.61 - \item [\hyperlink{command.apply_end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}~\isa{{\isachardoublequote}m{\isachardoublequote}}] applies proof method
4.62 + \item [\hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}~\isa{{\isachardoublequote}m{\isachardoublequote}}] applies proof method
4.63 \isa{m} as if in terminal position. Basically, this simulates a
4.64 multi-step tactic script for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, but may be given
4.65 anywhere within the proof body.
4.66 @@ -925,7 +925,7 @@
4.67 \indexdef{}{command}{finally}\hypertarget{command.finally}{\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
4.68 \indexdef{}{command}{moreover}\hypertarget{command.moreover}{\hyperlink{command.moreover}{\mbox{\isa{\isacommand{moreover}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
4.69 \indexdef{}{command}{ultimately}\hypertarget{command.ultimately}{\hyperlink{command.ultimately}{\mbox{\isa{\isacommand{ultimately}}}}} & : & \isartrans{proof(state)}{proof(chain)} \\
4.70 - \indexdef{}{command}{print\_trans\_rules}\hypertarget{command.print_trans_rules}{\hyperlink{command.print_trans_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
4.71 + \indexdef{}{command}{print\_trans\_rules}\hypertarget{command.print-trans-rules}{\hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
4.72 \hyperlink{attribute.trans}{\mbox{\isa{trans}}} & : & \isaratt \\
4.73 \hyperlink{attribute.sym}{\mbox{\isa{sym}}} & : & \isaratt \\
4.74 \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & : & \isaratt \\
4.75 @@ -997,7 +997,7 @@
4.76 analogous to \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, but collect
4.77 results only, without applying rules.
4.78
4.79 - \item [\hyperlink{command.print_trans_rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}] prints the list of
4.80 + \item [\hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}}] prints the list of
4.81 transitivity rules (for calculational commands \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} and
4.82 \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}) and symmetry rules (for the \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} operation and single step elimination patters) of the
4.83 current context.
5.1 --- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex Thu May 15 18:12:24 2008 +0200
5.2 +++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex Thu May 15 18:12:43 2008 +0200
5.3 @@ -154,14 +154,14 @@
5.4 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
5.5 \hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}} & no rules \\
5.6 \hyperlink{method.intro}{\mbox{\isa{intro}}}~\isa{a} & introduction rules \\
5.7 - \hyperlink{method.intro_classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} & class introduction rules \\
5.8 + \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} & class introduction rules \\
5.9 \hyperlink{method.elim}{\mbox{\isa{elim}}}~\isa{a} & elimination rules \\
5.10 \hyperlink{method.unfold}{\mbox{\isa{unfold}}}~\isa{a} & definitional rewrite rules \\[2ex]
5.11
5.12 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts)}} \\[0.5ex]
5.13 \hyperlink{method.iprover}{\mbox{\isa{iprover}}} & intuitionistic proof search \\
5.14 \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.fast}{\mbox{\isa{fast}}} & Classical Reasoner \\
5.15 - \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} & Simplifier (+ Splitter) \\
5.16 + \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} & Simplifier (+ Splitter) \\
5.17 \hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}} & Simplifier + Classical Reasoner \\
5.18 \hyperlink{method.arith}{\mbox{\isa{arith}}} & Arithmetic procedures \\
5.19 \end{tabular}%
5.20 @@ -180,8 +180,8 @@
5.21 \hyperlink{attribute.where}{\mbox{\isa{where}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} & rule instantiated with terms, by variable name \\
5.22 \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} & resolution with symmetry rule \\
5.23 \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{b} & resolution with another rule \\
5.24 - \hyperlink{attribute.rule_format}{\mbox{\isa{rule{\isacharunderscore}format}}} & result put into standard rule format \\
5.25 - \hyperlink{attribute.elim_format}{\mbox{\isa{elim{\isacharunderscore}format}}} & destruct rule turned into elimination rule format \\[1ex]
5.26 + \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} & result put into standard rule format \\
5.27 + \hyperlink{attribute.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}} & destruct rule turned into elimination rule format \\[1ex]
5.28
5.29 \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
5.30 \hyperlink{attribute.simp}{\mbox{\isa{simp}}} & Simplifier rule \\
5.31 @@ -201,7 +201,7 @@
5.32 \begin{isamarkuptext}%
5.33 \begin{tabular}{l|lllll}
5.34 & \hyperlink{method.rule}{\mbox{\isa{rule}}} & \hyperlink{method.iprover}{\mbox{\isa{iprover}}} & \hyperlink{method.blast}{\mbox{\isa{blast}}} & \hyperlink{method.simp}{\mbox{\isa{simp}}} & \hyperlink{method.auto}{\mbox{\isa{auto}}} \\
5.35 - & & & \hyperlink{method.fast}{\mbox{\isa{fast}}} & \hyperlink{method.simp_all}{\mbox{\isa{simp{\isacharunderscore}all}}} & \hyperlink{method.force}{\mbox{\isa{force}}} \\
5.36 + & & & \hyperlink{method.fast}{\mbox{\isa{fast}}} & \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} & \hyperlink{method.force}{\mbox{\isa{force}}} \\
5.37 \hline
5.38 \hyperlink{attribute.Pure.elim}{\mbox{\isa{Pure{\isachardot}elim}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} \hyperlink{attribute.Pure.intro}{\mbox{\isa{Pure{\isachardot}intro}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}
5.39 & \isa{{\isachardoublequote}{\isasymtimes}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymtimes}{\isachardoublequote}} \\
5.40 @@ -238,7 +238,7 @@
5.41 \begin{isamarkuptext}%
5.42 \begin{tabular}{ll}
5.43 \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{m} & apply proof method at initial position \\
5.44 - \hyperlink{command.apply_end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}~\isa{m} & apply proof method near terminal position \\
5.45 + \hyperlink{command.apply-end}{\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}}~\isa{m} & apply proof method near terminal position \\
5.46 \hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} & complete proof \\
5.47 \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}}~\isa{n} & move subgoal to end \\
5.48 \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}}~\isa{n} & move subgoal to beginning \\
5.49 @@ -253,19 +253,19 @@
5.50 %
5.51 \begin{isamarkuptext}%
5.52 \begin{tabular}{ll}
5.53 - \hyperlink{method.rule_tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}~\isa{insts} & resolution (with instantiation) \\
5.54 - \hyperlink{method.erule_tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}~\isa{insts} & elim-resolution (with instantiation) \\
5.55 - \hyperlink{method.drule_tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}~\isa{insts} & destruct-resolution (with instantiation) \\
5.56 - \hyperlink{method.frule_tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}~\isa{insts} & forward-resolution (with instantiation) \\
5.57 - \hyperlink{method.cut_tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}~\isa{insts} & insert facts (with instantiation) \\
5.58 - \hyperlink{method.thin_tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} & delete assumptions \\
5.59 - \hyperlink{method.subgoal_tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} & new claims \\
5.60 - \hyperlink{method.rename_tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{x} & rename innermost goal parameters \\
5.61 - \hyperlink{method.rotate_tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n} & rotate assumptions of goal \\
5.62 + \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}~\isa{insts} & resolution (with instantiation) \\
5.63 + \hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}~\isa{insts} & elim-resolution (with instantiation) \\
5.64 + \hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}~\isa{insts} & destruct-resolution (with instantiation) \\
5.65 + \hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}~\isa{insts} & forward-resolution (with instantiation) \\
5.66 + \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}~\isa{insts} & insert facts (with instantiation) \\
5.67 + \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} & delete assumptions \\
5.68 + \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} & new claims \\
5.69 + \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{x} & rename innermost goal parameters \\
5.70 + \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n} & rotate assumptions of goal \\
5.71 \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} & arbitrary ML tactic \\
5.72 - \hyperlink{method.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}}~\isa{t} & exhaustion (datatypes) \\
5.73 - \hyperlink{method.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}~\isa{x} & induction (datatypes) \\
5.74 - \hyperlink{method.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}~\isa{t} & exhaustion + simplification (inductive predicates) \\
5.75 + \hyperlink{method.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}~\isa{t} & exhaustion (datatypes) \\
5.76 + \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}~\isa{x} & induction (datatypes) \\
5.77 + \hyperlink{method.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}~\isa{t} & exhaustion + simplification (inductive predicates) \\
5.78 \end{tabular}%
5.79 \end{isamarkuptext}%
5.80 \isamarkuptrue%
6.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Thu May 15 18:12:24 2008 +0200
6.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Thu May 15 18:12:43 2008 +0200
6.3 @@ -36,7 +36,7 @@
6.4 Simplifier setup.
6.5
6.6 \begin{matharray}{rcl}
6.7 - \indexdef{ZF}{command}{print\_tcset}\hypertarget{command.ZF.print_tcset}{\hyperlink{command.ZF.print_tcset}{\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
6.8 + \indexdef{ZF}{command}{print\_tcset}\hypertarget{command.ZF.print-tcset}{\hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
6.9 \indexdef{ZF}{method}{typecheck}\hypertarget{method.ZF.typecheck}{\hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}}} & : & \isarmeth \\
6.10 \indexdef{ZF}{attribute}{TC}\hypertarget{attribute.ZF.TC}{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}} & : & \isaratt \\
6.11 \end{matharray}
6.12 @@ -48,7 +48,7 @@
6.13
6.14 \begin{descr}
6.15
6.16 - \item [\hyperlink{command.ZF.print_tcset}{\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}}] prints the collection of
6.17 + \item [\hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}}] prints the collection of
6.18 typechecking rules of the current context.
6.19
6.20 \item [\hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}}] attempts to solve any pending
6.21 @@ -148,10 +148,10 @@
6.22 ported to Isar. These should not be used in proper proof texts.
6.23
6.24 \begin{matharray}{rcl}
6.25 - \indexdef{ZF}{method}{case\_tac}\hypertarget{method.ZF.case_tac}{\hyperlink{method.ZF.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
6.26 - \indexdef{ZF}{method}{induct\_tac}\hypertarget{method.ZF.induct_tac}{\hyperlink{method.ZF.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
6.27 - \indexdef{ZF}{method}{ind\_cases}\hypertarget{method.ZF.ind_cases}{\hyperlink{method.ZF.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
6.28 - \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive_cases}{\hyperlink{command.ZF.inductive_cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
6.29 + \indexdef{ZF}{method}{case\_tac}\hypertarget{method.ZF.case-tac}{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
6.30 + \indexdef{ZF}{method}{induct\_tac}\hypertarget{method.ZF.induct-tac}{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
6.31 + \indexdef{ZF}{method}{ind\_cases}\hypertarget{method.ZF.ind-cases}{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
6.32 + \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive-cases}{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
6.33 \end{matharray}
6.34
6.35 \begin{rail}
7.1 --- a/doc-src/IsarRef/Thy/document/pdfsetup.sty Thu May 15 18:12:24 2008 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,25 +0,0 @@
7.4 -%%
7.5 -%%
7.6 -%%
7.7 -%% smart url or hyperref setup
7.8 -%%
7.9 -
7.10 -\newif\ifpdfoutput
7.11 -\ifx\pdfoutput\undefined
7.12 -\else
7.13 - \ifx\pdfoutput\relax
7.14 - \else
7.15 - \ifcase\pdfoutput
7.16 - \else\pdfoutputtrue\fi
7.17 - \fi
7.18 -\fi
7.19 -
7.20 -\ifpdfoutput
7.21 - \message{PDF output}
7.22 - \usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
7.23 - \usepackage[pdftex,a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
7.24 - \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}
7.25 -\else
7.26 - \message{No PDF output}
7.27 - \usepackage{url}
7.28 -\fi
8.1 --- a/doc-src/IsarRef/Thy/document/pure.tex Thu May 15 18:12:24 2008 +0200
8.2 +++ b/doc-src/IsarRef/Thy/document/pure.tex Thu May 15 18:12:43 2008 +0200
8.3 @@ -63,7 +63,7 @@
8.4 \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
8.5 \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
8.6 \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\
8.7 - \indexdef{}{command}{text\_raw}\hypertarget{command.text_raw}{\hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\
8.8 + \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\
8.9 \end{matharray}
8.10
8.11 Apart from formal comments (see \secref{sec:comments}), markup
8.12 @@ -85,14 +85,14 @@
8.13
8.14 \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}] specifies paragraphs of plain text.
8.15
8.16 - \item [\hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}] inserts {\LaTeX} source into the
8.17 + \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}] inserts {\LaTeX} source into the
8.18 output, without additional markup. Thus the full range of document
8.19 manipulations becomes available.
8.20
8.21 \end{descr}
8.22
8.23 The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
8.24 - \hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
8.25 + \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
8.26 (``antiquotations'', see also \secref{sec:antiq}). These are
8.27 interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
8.28
8.29 @@ -101,7 +101,7 @@
8.30 commands this is a plain macro with a single argument, e.g.\
8.31 \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
8.32 \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}. The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a
8.33 - {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text_raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}
8.34 + {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}
8.35 causes the text to be inserted directly into the {\LaTeX} source.
8.36
8.37 \medskip Additional markup commands are available for proofs (see
8.38 @@ -119,7 +119,7 @@
8.39 \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
8.40 \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
8.41 \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
8.42 - \indexdef{}{command}{class\_deps}\hypertarget{command.class_deps}{\hyperlink{command.class_deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
8.43 + \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
8.44 \end{matharray}
8.45
8.46 \begin{rail}
8.47 @@ -146,7 +146,7 @@
8.48 constraints. Usually, the default sort would be only changed when
8.49 defining a new object-logic.
8.50
8.51 - \item [\hyperlink{command.class_deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
8.52 + \item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
8.53 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
8.54
8.55 \end{descr}%
8.56 @@ -315,9 +315,9 @@
8.57 \begin{isamarkuptext}%
8.58 \begin{matharray}{rcl}
8.59 \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\
8.60 - \indexdef{}{command}{no\_syntax}\hypertarget{command.no_syntax}{\hyperlink{command.no_syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
8.61 + \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
8.62 \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\
8.63 - \indexdef{}{command}{no\_translations}\hypertarget{command.no_translations}{\hyperlink{command.no_translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\
8.64 + \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\
8.65 \end{matharray}
8.66
8.67 \begin{rail}
8.68 @@ -342,7 +342,7 @@
8.69 print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
8.70 input and output grammar.
8.71
8.72 - \item [\hyperlink{command.no_syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
8.73 + \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
8.74 grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
8.75
8.76 \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic
8.77 @@ -351,7 +351,7 @@
8.78 Translation patterns may be prefixed by the syntactic category to be
8.79 used for parsing; the default is \isa{logic}.
8.80
8.81 - \item [\hyperlink{command.no_translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
8.82 + \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
8.83 translation rules, which are interpreted in the same manner as for
8.84 \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
8.85
8.86 @@ -456,10 +456,10 @@
8.87 \begin{matharray}{rcl}
8.88 \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
8.89 \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
8.90 - \indexdef{}{command}{ML\_val}\hypertarget{command.ML_val}{\hyperlink{command.ML_val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
8.91 - \indexdef{}{command}{ML\_command}\hypertarget{command.ML_command}{\hyperlink{command.ML_command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
8.92 + \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
8.93 + \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
8.94 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
8.95 - \indexdef{}{command}{method\_setup}\hypertarget{command.method_setup}{\hyperlink{command.method_setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\
8.96 + \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\
8.97 \end{matharray}
8.98
8.99 \begin{rail}
8.100 @@ -481,10 +481,10 @@
8.101
8.102 \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
8.103
8.104 - \item [\hyperlink{command.ML_val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML_command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
8.105 + \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
8.106 diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context
8.107 - may not be updated. \hyperlink{command.ML_val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
8.108 - at the ML toplevel, but \hyperlink{command.ML_command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
8.109 + may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
8.110 + at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
8.111
8.112 \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
8.113 context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
8.114 @@ -492,7 +492,7 @@
8.115 any object-logic specific tools and packages written in ML, for
8.116 example.
8.117
8.118 - \item [\hyperlink{command.method_setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
8.119 + \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
8.120 defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%
8.121 \verb| Proof.context -> Proof.method"|. Parsing concrete method syntax
8.122 from \verb|Args.src| input can be quite tedious in general. The
8.123 @@ -526,12 +526,12 @@
8.124 %
8.125 \begin{isamarkuptext}%
8.126 \begin{matharray}{rcl}
8.127 - \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse_ast_translation}{\hyperlink{command.parse_ast_translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.128 - \indexdef{}{command}{parse\_translation}\hypertarget{command.parse_translation}{\hyperlink{command.parse_translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.129 - \indexdef{}{command}{print\_translation}\hypertarget{command.print_translation}{\hyperlink{command.print_translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.130 - \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed_print_translation}{\hyperlink{command.typed_print_translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.131 - \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print_ast_translation}{\hyperlink{command.print_ast_translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.132 - \indexdef{}{command}{token\_translation}\hypertarget{command.token_translation}{\hyperlink{command.token_translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.133 + \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.134 + \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.135 + \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.136 + \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.137 + \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.138 + \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
8.139 \end{matharray}
8.140
8.141 \begin{rail}
8.142 @@ -634,7 +634,7 @@
8.143 \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\
8.144 \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\
8.145 \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\
8.146 - \indexdef{}{command}{txt\_raw}\hypertarget{command.txt_raw}{\hyperlink{command.txt_raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\
8.147 + \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\
8.148 \end{matharray}
8.149
8.150 These markup commands for proof mode closely correspond to the ones
8.151 @@ -663,7 +663,7 @@
8.152 \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.153 \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.154 \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.155 - \indexdef{}{command}{full\_prf}\hypertarget{command.full_prf}{\hyperlink{command.full_prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.156 + \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.157 \end{matharray}
8.158
8.159 These diagnostic commands assist interactive development. Note that
8.160 @@ -719,7 +719,7 @@
8.161 object logic (see the ``Proof terms'' section of the Isabelle
8.162 reference manual for information on how to do this).
8.163
8.164 - \item [\hyperlink{command.full_prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
8.165 + \item [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
8.166 the full proof term, i.e.\ also displays information omitted in the
8.167 compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
8.168 there.
8.169 @@ -746,16 +746,16 @@
8.170 %
8.171 \begin{isamarkuptext}%
8.172 \begin{matharray}{rcl}
8.173 - \indexdef{}{command}{print\_commands}\hypertarget{command.print_commands}{\hyperlink{command.print_commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.174 - \indexdef{}{command}{print\_theory}\hypertarget{command.print_theory}{\hyperlink{command.print_theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.175 - \indexdef{}{command}{print\_syntax}\hypertarget{command.print_syntax}{\hyperlink{command.print_syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.176 - \indexdef{}{command}{print\_methods}\hypertarget{command.print_methods}{\hyperlink{command.print_methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.177 - \indexdef{}{command}{print\_attributes}\hypertarget{command.print_attributes}{\hyperlink{command.print_attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.178 - \indexdef{}{command}{print\_theorems}\hypertarget{command.print_theorems}{\hyperlink{command.print_theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.179 - \indexdef{}{command}{find\_theorems}\hypertarget{command.find_theorems}{\hyperlink{command.find_theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.180 - \indexdef{}{command}{thm\_deps}\hypertarget{command.thm_deps}{\hyperlink{command.thm_deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.181 - \indexdef{}{command}{print\_facts}\hypertarget{command.print_facts}{\hyperlink{command.print_facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
8.182 - \indexdef{}{command}{print\_binds}\hypertarget{command.print_binds}{\hyperlink{command.print_binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
8.183 + \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.184 + \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.185 + \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.186 + \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.187 + \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.188 + \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.189 + \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.190 + \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
8.191 + \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
8.192 + \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
8.193 \end{matharray}
8.194
8.195 \begin{rail}
8.196 @@ -777,29 +777,29 @@
8.197
8.198 \begin{descr}
8.199
8.200 - \item [\hyperlink{command.print_commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory
8.201 + \item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory
8.202 syntax, including keywords and command.
8.203
8.204 - \item [\hyperlink{command.print_theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of
8.205 + \item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of
8.206 the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
8.207 verbosity.
8.208
8.209 - \item [\hyperlink{command.print_syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types
8.210 + \item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types
8.211 and terms, depending on the current context. The output can be very
8.212 verbose, including grammar tables and syntax translation rules. See
8.213 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
8.214 inner syntax.
8.215
8.216 - \item [\hyperlink{command.print_methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods
8.217 + \item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods
8.218 available in the current theory context.
8.219
8.220 - \item [\hyperlink{command.print_attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes
8.221 + \item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes
8.222 available in the current theory context.
8.223
8.224 - \item [\hyperlink{command.print_theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from
8.225 + \item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from
8.226 the last command.
8.227
8.228 - \item [\hyperlink{command.find_theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts
8.229 + \item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts
8.230 from the theory or proof context matching all of given search
8.231 criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
8.232 whose fully qualified name matches pattern \isa{p}, which may
8.233 @@ -818,14 +818,14 @@
8.234 default, duplicates are removed from the search result. Use
8.235 \isa{with{\isacharunderscore}dups} to display duplicates.
8.236
8.237 - \item [\hyperlink{command.thm_deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
8.238 + \item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
8.239 visualizes dependencies of facts, using Isabelle's graph browser
8.240 tool (see also \cite{isabelle-sys}).
8.241
8.242 - \item [\hyperlink{command.print_facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the
8.243 + \item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the
8.244 current context, both named and unnamed ones.
8.245
8.246 - \item [\hyperlink{command.print_binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations
8.247 + \item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations
8.248 present in the context.
8.249
8.250 \end{descr}%
8.251 @@ -870,9 +870,9 @@
8.252 \begin{matharray}{rcl}
8.253 \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.254 \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.255 - \indexdef{}{command}{use\_thy}\hypertarget{command.use_thy}{\hyperlink{command.use_thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.256 - \indexdef{}{command}{display\_drafts}\hypertarget{command.display_drafts}{\hyperlink{command.display_drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.257 - \indexdef{}{command}{print\_drafts}\hypertarget{command.print_drafts}{\hyperlink{command.print_drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.258 + \indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.259 + \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.260 + \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
8.261 \end{matharray}
8.262
8.263 \begin{rail}
8.264 @@ -889,11 +889,11 @@
8.265
8.266 \item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory.
8.267
8.268 - \item [\hyperlink{command.use_thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}.
8.269 + \item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}.
8.270 These system commands are scarcely used when working interactively,
8.271 since loading of theories is done automatically as required.
8.272
8.273 - \item [\hyperlink{command.display_drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print_drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths}] perform simple output of a given list
8.274 + \item [\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths}] perform simple output of a given list
8.275 of raw source files. Only those symbols that do not require
8.276 additional {\LaTeX} packages are displayed properly, everything else
8.277 is left verbatim.
9.1 --- a/doc-src/IsarRef/Thy/document/syntax.tex Thu May 15 18:12:24 2008 +0200
9.2 +++ b/doc-src/IsarRef/Thy/document/syntax.tex Thu May 15 18:12:43 2008 +0200
9.3 @@ -510,16 +510,16 @@
9.4 \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
9.5 \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
9.6 \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
9.7 - \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm_style}{\hyperlink{antiquotation.thm_style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
9.8 - \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term_style}{\hyperlink{antiquotation.term_style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
9.9 + \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
9.10 + \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
9.11 \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
9.12 \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
9.13 \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
9.14 \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
9.15 - \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full_prf}{\hyperlink{antiquotation.full_prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
9.16 + \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
9.17 \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
9.18 - \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML_type}{\hyperlink{antiquotation.ML_type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
9.19 - \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML_struct}{\hyperlink{antiquotation.ML_struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\
9.20 + \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
9.21 + \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\
9.22 \end{matharray}
9.23
9.24 The text body of formal comments (see also \secref{sec:comments})
9.25 @@ -579,7 +579,7 @@
9.26 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
9.27 \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
9.28 may be included as well (see also \secref{sec:syn-att}); the
9.29 - \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no_vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
9.30 + \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
9.31 be particularly useful to suppress printing of schematic variables.
9.32
9.33 \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.