# HG changeset patch # User wenzelm # Date 1236630333 -3600 # Node ID b6212ae2165650e83e70bf1b84f02b888536390f # Parent 841ce0fcbe144f6222685b8366a763dd5dbc6718 markup antiquotation options; more correct references to external manuals; diff -r 841ce0fcbe14 -r b6212ae21656 doc-src/IsarRef/Thy/Document_Preparation.thy --- 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 - \}-contracted form. + \item @{antiquotation_option_def eta_contract}~@{text "= bool"} + prints terms in @{text \}-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} diff -r 841ce0fcbe14 -r b6212ae21656 doc-src/IsarRef/Thy/Generic.thy --- 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 \ a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1 - \ a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \ 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 \ a\<^sub>n"}, @{method + drule}~@{text "a\<^sub>1 \ a\<^sub>n"}, and @{method frule}~@{text + "a\<^sub>1 \ 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 \ a\<^sub>n"} and @{attribute folded}~@{text "a\<^sub>1 \ 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 \} deletes the specified assumption from a subgoal; note that @{text \} 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 \} adds @{text \} 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 \ x\<^sub>n"} renames parameters of a goal according to the list @{text "x\<^sub>1, \, 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. diff -r 841ce0fcbe14 -r b6212ae21656 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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} diff -r 841ce0fcbe14 -r b6212ae21656 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- 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} diff -r 841ce0fcbe14 -r b6212ae21656 doc-src/IsarRef/Thy/document/Generic.tex --- 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. diff -r 841ce0fcbe14 -r b6212ae21656 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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}