--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Mar 09 21:23:40 2009 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Mar 09 21:25:33 2009 +0100
@@ -317,61 +317,63 @@
\begin{description}
- \item @{text "show_types = bool"} and @{text "show_sorts = bool"}
- control printing of explicit type and sort constraints.
+ \item @{antiquotation_option_def show_types}~@{text "= bool"} and
+ @{antiquotation_option_def show_sorts}~@{text "= bool"} control
+ printing of explicit type and sort constraints.
- \item @{text "show_structs = bool"} controls printing of implicit
- structures.
+ \item @{antiquotation_option_def show_structs}~@{text "= bool"}
+ controls printing of implicit structures.
- \item @{text "long_names = bool"} forces names of types and
- constants etc.\ to be printed in their fully qualified internal
- form.
+ \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
+ names of types and constants etc.\ to be printed in their fully
+ qualified internal form.
- \item @{text "short_names = bool"} forces names of types and
- constants etc.\ to be printed unqualified. Note that internalizing
- the output again in the current context may well yield a different
- result.
+ \item @{antiquotation_option_def short_names}~@{text "= bool"}
+ forces names of types and constants etc.\ to be printed unqualified.
+ Note that internalizing the output again in the current context may
+ well yield a different result.
- \item @{text "unique_names = bool"} determines whether the printed
- version of qualified names should be made sufficiently long to avoid
- overlap with names declared further back. Set to @{text false} for
- more concise output.
+ \item @{antiquotation_option_def unique_names}~@{text "= bool"}
+ determines whether the printed version of qualified names should be
+ made sufficiently long to avoid overlap with names declared further
+ back. Set to @{text false} for more concise output.
- \item @{text "eta_contract = bool"} prints terms in @{text
- \<eta>}-contracted form.
+ \item @{antiquotation_option_def eta_contract}~@{text "= bool"}
+ prints terms in @{text \<eta>}-contracted form.
- \item @{text "display = bool"} indicates if the text is to be output
- as multi-line ``display material'', rather than a small piece of
- text without line breaks (which is the default).
+ \item @{antiquotation_option_def display}~@{text "= bool"} indicates
+ if the text is to be output as multi-line ``display material'',
+ rather than a small piece of text without line breaks (which is the
+ default).
In this mode the embedded entities are printed in the same style as
the main theory text.
- \item @{text "break = bool"} controls line breaks in non-display
- material.
+ \item @{antiquotation_option_def break}~@{text "= bool"} controls
+ line breaks in non-display material.
- \item @{text "quotes = bool"} indicates if the output should be
- enclosed in double quotes.
+ \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates
+ if the output should be enclosed in double quotes.
- \item @{text "mode = name"} adds @{text name} to the print mode to
- be used for presentation (see also \cite{isabelle-ref}). Note that
- the standard setup for {\LaTeX} output is already present by
- default, including the modes @{text latex} and @{text xsymbols}.
+ \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text
+ name} to the print mode to be used for presentation. Note that the
+ standard setup for {\LaTeX} output is already present by default,
+ including the modes @{text latex} and @{text xsymbols}.
- \item @{text "margin = nat"} and @{text "indent = nat"} change the
- margin or indentation for pretty printing of display material.
-
- \item @{text "goals_limit = nat"} determines the maximum number of
- goals to be printed (for goal-based antiquotation).
+ \item @{antiquotation_option_def margin}~@{text "= nat"} and
+ @{antiquotation_option_def indent}~@{text "= nat"} change the margin
+ or indentation for pretty printing of display material.
- \item @{text "locale = name"} specifies an alternative locale
- context used for evaluating and printing the subsequent argument.
+ \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
+ determines the maximum number of goals to be printed (for goal-based
+ antiquotation).
- \item @{text "source = bool"} prints the original source text of the
- antiquotation arguments, rather than its internal representation.
- Note that formal checking of @{antiquotation "thm"}, @{antiquotation
- "term"}, etc. is still enabled; use the @{antiquotation "text"}
- antiquotation for unchecked output.
+ \item @{antiquotation_option_def source}~@{text "= bool"} prints the
+ original source text of the antiquotation arguments, rather than its
+ internal representation. Note that formal checking of
+ @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
+ enabled; use the @{antiquotation "text"} antiquotation for unchecked
+ output.
Regular @{text "term"} and @{text "typ"} antiquotations with @{text
"source = false"} involve a full round-trip from the original source
@@ -380,9 +382,10 @@
not under direct control of the author, it may even fluctuate a bit
as the underlying theory is changed later on.
- In contrast, @{text "source = true"} admits direct printing of the
- given source text, with the desirable well-formedness check in the
- background, but without modification of the printed text.
+ In contrast, @{antiquotation_option_def source}~@{text "= true"}
+ admits direct printing of the given source text, with the desirable
+ well-formedness check in the background, but without modification of
+ the printed text.
\end{description}
--- a/doc-src/IsarRef/Thy/Generic.thy Mon Mar 09 21:23:40 2009 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon Mar 09 21:25:33 2009 +0100
@@ -78,13 +78,14 @@
into all goals of the proof state. Note that current facts
indicated for forward chaining are ignored.
- \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1
- \<dots> a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the
- basic @{method rule} method (see \secref{sec:pure-meth-att}), but
- apply rules by elim-resolution, destruct-resolution, and
- forward-resolution, respectively \cite{isabelle-ref}. The optional
- natural number argument (default 0) specifies additional assumption
- steps to be performed here.
+ \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
+ drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
+ "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
+ method (see \secref{sec:pure-meth-att}), but apply rules by
+ elim-resolution, destruct-resolution, and forward-resolution,
+ respectively \cite{isabelle-implementation}. The optional natural
+ number argument (default 0) specifies additional assumption steps to
+ be performed here.
Note that these methods are improper ones, mainly serving for
experimentation and tactic script emulation. Different modes of
@@ -143,7 +144,7 @@
specified); the @{attribute COMP} version skips the automatic
lifting process that is normally intended (cf.\ @{ML [source=false]
"op RS"} and @{ML [source=false] "op COMP"} in
- \cite[\S5]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
@@ -304,26 +305,26 @@
\item @{method rule_tac} etc. do resolution of rules with explicit
instantiation. This works the same way as the ML tactics @{ML
- res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
+ res_inst_tac} etc. (see \cite{isabelle-implementation})
Multiple rules may be only given if there is no instantiation; then
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
- \cite[\S3]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item @{method cut_tac} inserts facts into the proof state as
assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
- \cite[\S3]{isabelle-ref}. Note that the scope of schematic
+ \cite{isabelle-implementation}. Note that the scope of schematic
variables is spread over the main goal statement. Instantiations
may be given as well, see also ML tactic @{ML cut_inst_tac} in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
from a subgoal; note that @{text \<phi>} may contain schematic variables.
- See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
+ See also @{ML thin_tac} in \cite{isabelle-implementation}.
\item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
- subgoals_tac} in \cite[\S3]{isabelle-ref}.
+ subgoals_tac} in \cite{isabelle-implementation}.
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
@@ -333,7 +334,7 @@
goal by @{text n} positions: from right to left if @{text n} is
positive, and from left to right if @{text n} is negative; the
default value is 1. See also @{ML rotate_tac} in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item @{method tactic}~@{text "text"} produces a proof method from
any ML text of type @{ML_type tactic}. Apart from the usual ML
@@ -400,13 +401,13 @@
By default the Simplifier methods take local assumptions fully into
account, using equational assumptions in the subsequent
normalization process, or simplifying assumptions themselves (cf.\
- @{ML asm_full_simp_tac} in \cite[\S10]{isabelle-ref}). In
- structured proofs this is usually quite well behaved in practice:
- just the local premises of the actual goal are involved, additional
- facts may be inserted via explicit forward-chaining (via @{command
- "then"}, @{command "from"}, @{command "using"} etc.). The full
- context of premises is only included if the ``@{text "!"}'' (bang)
- argument is given, which should be used with some care, though.
+ @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured
+ proofs this is usually quite well behaved in practice: just the
+ local premises of the actual goal are involved, additional facts may
+ be inserted via explicit forward-chaining (via @{command "then"},
+ @{command "from"}, @{command "using"} etc.). The full context of
+ premises is only included if the ``@{text "!"}'' (bang) argument is
+ given, which should be used with some care, though.
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -615,14 +616,14 @@
\begin{description}
\item @{method blast} refers to the classical tableau prover (see
- @{ML blast_tac} in \cite[\S11]{isabelle-ref}). The optional
- argument specifies a user-supplied search bound (default 20).
+ @{ML blast_tac} in \cite{isabelle-ref}). The optional argument
+ specifies a user-supplied search bound (default 20).
\item @{method fast}, @{method slow}, @{method best}, @{method
safe}, and @{method clarify} refer to the generic classical
reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
- safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for
- more information.
+ safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
+ information.
\end{description}
@@ -667,8 +668,8 @@
to Isabelle's combined simplification and classical reasoning
tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
- added as wrapper, see \cite[\S11]{isabelle-ref} for more
- information. The modifier arguments correspond to those given in
+ added as wrapper, see \cite{isabelle-ref} for more information. The
+ modifier arguments correspond to those given in
\secref{sec:simplifier} and \secref{sec:classical}. Just note that
the ones related to the Simplifier are prefixed by \railtterm{simp}
here.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 09 21:23:40 2009 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 09 21:25:33 2009 +0100
@@ -799,8 +799,8 @@
translations functions may refer to specific theory declarations or
auxiliary proof data.
- See also \cite[\S8]{isabelle-ref} for more information on the
- general concept of syntax transformations in Isabelle.
+ See also \cite{isabelle-ref} for more information on the general
+ concept of syntax transformations in Isabelle.
%FIXME proper antiquotations
\begin{ttbox}
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Mar 09 21:23:40 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Mar 09 21:25:33 2009 +0100
@@ -335,59 +335,62 @@
\begin{description}
- \item \isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}
- control printing of explicit type and sort constraints.
+ \item \indexdef{}{antiquotation option}{show\_types}\hypertarget{antiquotation option.show-types}{\hyperlink{antiquotation option.show-types}{\mbox{\isa{show{\isacharunderscore}types}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} and
+ \indexdef{}{antiquotation option}{show\_sorts}\hypertarget{antiquotation option.show-sorts}{\hyperlink{antiquotation option.show-sorts}{\mbox{\isa{show{\isacharunderscore}sorts}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} control
+ printing of explicit type and sort constraints.
- \item \isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}} controls printing of implicit
- structures.
+ \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isacharunderscore}structs}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ controls printing of implicit structures.
- \item \isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
- constants etc.\ to be printed in their fully qualified internal
- form.
+ \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} forces
+ names of types and constants etc.\ to be printed in their fully
+ qualified internal form.
- \item \isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
- constants etc.\ to be printed unqualified. Note that internalizing
- the output again in the current context may well yield a different
- result.
+ \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ forces names of types and constants etc.\ to be printed unqualified.
+ Note that internalizing the output again in the current context may
+ well yield a different result.
- \item \isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} determines whether the printed
- version of qualified names should be made sufficiently long to avoid
- overlap with names declared further back. Set to \isa{false} for
- more concise output.
+ \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ determines whether the printed version of qualified names should be
+ made sufficiently long to avoid overlap with names declared further
+ back. Set to \isa{false} for more concise output.
- \item \isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}} prints terms in \isa{{\isasymeta}}-contracted form.
+ \item \indexdef{}{antiquotation option}{eta\_contract}\hypertarget{antiquotation option.eta-contract}{\hyperlink{antiquotation option.eta-contract}{\mbox{\isa{eta{\isacharunderscore}contract}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ prints terms in \isa{{\isasymeta}}-contracted form.
- \item \isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the text is to be output
- as multi-line ``display material'', rather than a small piece of
- text without line breaks (which is the default).
+ \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
+ if the text is to be output as multi-line ``display material'',
+ rather than a small piece of text without line breaks (which is the
+ default).
In this mode the embedded entities are printed in the same style as
the main theory text.
- \item \isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}} controls line breaks in non-display
- material.
+ \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
+ line breaks in non-display material.
- \item \isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the output should be
- enclosed in double quotes.
+ \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
+ if the output should be enclosed in double quotes.
- \item \isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to
- be used for presentation (see also \cite{isabelle-ref}). Note that
- the standard setup for {\LaTeX} output is already present by
- default, including the modes \isa{latex} and \isa{xsymbols}.
+ \item \indexdef{}{antiquotation option}{mode}\hypertarget{antiquotation option.mode}{\hyperlink{antiquotation option.mode}{\mbox{\isa{mode}}}}~\isa{{\isachardoublequote}{\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to be used for presentation. Note that the
+ standard setup for {\LaTeX} output is already present by default,
+ including the modes \isa{latex} and \isa{xsymbols}.
- \item \isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}} change the
- margin or indentation for pretty printing of display material.
-
- \item \isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}} determines the maximum number of
- goals to be printed (for goal-based antiquotation).
+ \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
+ \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
+ or indentation for pretty printing of display material.
- \item \isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}} specifies an alternative locale
- context used for evaluating and printing the subsequent argument.
+ \item \indexdef{}{antiquotation option}{goals\_limit}\hypertarget{antiquotation option.goals-limit}{\hyperlink{antiquotation option.goals-limit}{\mbox{\isa{goals{\isacharunderscore}limit}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}}
+ determines the maximum number of goals to be printed (for goal-based
+ antiquotation).
- \item \isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}} prints the original source text of the
- antiquotation arguments, rather than its internal representation.
- Note that formal checking of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}}
- antiquotation for unchecked output.
+ \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
+ original source text of the antiquotation arguments, rather than its
+ internal representation. Note that formal checking of
+ \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
+ enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
+ output.
Regular \isa{{\isachardoublequote}term{\isachardoublequote}} and \isa{{\isachardoublequote}typ{\isachardoublequote}} antiquotations with \isa{{\isachardoublequote}source\ {\isacharequal}\ false{\isachardoublequote}} involve a full round-trip from the original source
to an internalized logical entity back to a source form, according
@@ -395,9 +398,10 @@
not under direct control of the author, it may even fluctuate a bit
as the underlying theory is changed later on.
- In contrast, \isa{{\isachardoublequote}source\ {\isacharequal}\ true{\isachardoublequote}} admits direct printing of the
- given source text, with the desirable well-formedness check in the
- background, but without modification of the printed text.
+ In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
+ admits direct printing of the given source text, with the desirable
+ well-formedness check in the background, but without modification of
+ the printed text.
\end{description}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon Mar 09 21:23:40 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon Mar 09 21:25:33 2009 +0100
@@ -99,12 +99,12 @@
into all goals of the proof state. Note that current facts
indicated for forward chaining are ignored.
- \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} are similar to the
- basic \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see \secref{sec:pure-meth-att}), but
- apply rules by elim-resolution, destruct-resolution, and
- forward-resolution, respectively \cite{isabelle-ref}. The optional
- natural number argument (default 0) specifies additional assumption
- steps to be performed here.
+ \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} are similar to the basic \hyperlink{method.rule}{\mbox{\isa{rule}}}
+ method (see \secref{sec:pure-meth-att}), but apply rules by
+ elim-resolution, destruct-resolution, and forward-resolution,
+ respectively \cite{isabelle-implementation}. The optional natural
+ number argument (default 0) specifies additional assumption steps to
+ be performed here.
Note that these methods are improper ones, mainly serving for
experimentation and tactic script emulation. Different modes of
@@ -161,7 +161,7 @@
first premise of \isa{a} (an alternative position may be also
specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
lifting process that is normally intended (cf.\ \verb|op RS| and \verb|op COMP| in
- \cite[\S5]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand and fold back again the given
definitions throughout a rule.
@@ -321,25 +321,25 @@
\begin{description}
\item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc. do resolution of rules with explicit
- instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref})
+ instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
Multiple rules may be only given if there is no instantiation; then
\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
- \cite[\S3]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}} inserts facts into the proof state as
assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
- \cite[\S3]{isabelle-ref}. Note that the scope of schematic
+ \cite{isabelle-implementation}. Note that the scope of schematic
variables is spread over the main goal statement. Instantiations
may be given as well, see also ML tactic \verb|cut_inst_tac| in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} deletes the specified assumption
from a subgoal; note that \isa{{\isasymphi}} may contain schematic variables.
- See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
+ See also \verb|thin_tac| in \cite{isabelle-implementation}.
\item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} adds \isa{{\isasymphi}} as an
- assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
+ assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
\item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} renames 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
@@ -349,7 +349,7 @@
goal by \isa{n} positions: from right to left if \isa{n} is
positive, and from left to right if \isa{n} is negative; the
default value is 1. See also \verb|rotate_tac| in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} produces a proof method from
any ML text of type \verb|tactic|. Apart from the usual ML
@@ -420,12 +420,13 @@
By default the Simplifier methods take local assumptions fully into
account, using equational assumptions in the subsequent
normalization process, or simplifying assumptions themselves (cf.\
- \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}). In
- structured proofs this is usually quite well behaved in practice:
- just the local premises of the actual goal are involved, additional
- facts may be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}, \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full
- context of premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang)
- argument is given, which should be used with some care, though.
+ \verb|asm_full_simp_tac| in \cite{isabelle-ref}). In structured
+ proofs this is usually quite well behaved in practice: just the
+ local premises of the actual goal are involved, additional facts may
+ be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
+ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full context of
+ premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
+ given, which should be used with some care, though.
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -637,12 +638,12 @@
\begin{description}
\item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
- \verb|blast_tac| in \cite[\S11]{isabelle-ref}). The optional
- argument specifies a user-supplied search bound (default 20).
+ \verb|blast_tac| in \cite{isabelle-ref}). The optional argument
+ specifies a user-supplied search bound (default 20).
\item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.safe}{\mbox{\isa{safe}}}, and \hyperlink{method.clarify}{\mbox{\isa{clarify}}} refer to the generic classical
- reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite[\S11]{isabelle-ref} for
- more information.
+ reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
+ information.
\end{description}
@@ -686,8 +687,8 @@
\item \hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}}, \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}, \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, and \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} provide access
to Isabelle's combined simplification and classical reasoning
tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
- added as wrapper, see \cite[\S11]{isabelle-ref} for more
- information. The modifier arguments correspond to those given in
+ added as wrapper, see \cite{isabelle-ref} for more information. The
+ modifier arguments correspond to those given in
\secref{sec:simplifier} and \secref{sec:classical}. Just note that
the ones related to the Simplifier are prefixed by \railtterm{simp}
here.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 09 21:23:40 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 09 21:25:33 2009 +0100
@@ -819,8 +819,8 @@
translations functions may refer to specific theory declarations or
auxiliary proof data.
- See also \cite[\S8]{isabelle-ref} for more information on the
- general concept of syntax transformations in Isabelle.
+ See also \cite{isabelle-ref} for more information on the general
+ concept of syntax transformations in Isabelle.
%FIXME proper antiquotations
\begin{ttbox}