markup antiquotation options;
authorwenzelm
Mon Mar 09 21:25:33 2009 +0100 (2009-03-09)
changeset 30397b6212ae21656
parent 30396 841ce0fcbe14
child 30398 d7ac4b7aa590
markup antiquotation options;
more correct references to external manuals;
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
     1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Mar 09 21:23:40 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Mar 09 21:25:33 2009 +0100
     1.3 @@ -317,61 +317,63 @@
     1.4  
     1.5    \begin{description}
     1.6  
     1.7 -  \item @{text "show_types = bool"} and @{text "show_sorts = bool"}
     1.8 -  control printing of explicit type and sort constraints.
     1.9 +  \item @{antiquotation_option_def show_types}~@{text "= bool"} and
    1.10 +  @{antiquotation_option_def show_sorts}~@{text "= bool"} control
    1.11 +  printing of explicit type and sort constraints.
    1.12  
    1.13 -  \item @{text "show_structs = bool"} controls printing of implicit
    1.14 -  structures.
    1.15 +  \item @{antiquotation_option_def show_structs}~@{text "= bool"}
    1.16 +  controls printing of implicit structures.
    1.17  
    1.18 -  \item @{text "long_names = bool"} forces names of types and
    1.19 -  constants etc.\ to be printed in their fully qualified internal
    1.20 -  form.
    1.21 +  \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
    1.22 +  names of types and constants etc.\ to be printed in their fully
    1.23 +  qualified internal form.
    1.24  
    1.25 -  \item @{text "short_names = bool"} forces names of types and
    1.26 -  constants etc.\ to be printed unqualified.  Note that internalizing
    1.27 -  the output again in the current context may well yield a different
    1.28 -  result.
    1.29 +  \item @{antiquotation_option_def short_names}~@{text "= bool"}
    1.30 +  forces names of types and constants etc.\ to be printed unqualified.
    1.31 +  Note that internalizing the output again in the current context may
    1.32 +  well yield a different result.
    1.33  
    1.34 -  \item @{text "unique_names = bool"} determines whether the printed
    1.35 -  version of qualified names should be made sufficiently long to avoid
    1.36 -  overlap with names declared further back.  Set to @{text false} for
    1.37 -  more concise output.
    1.38 +  \item @{antiquotation_option_def unique_names}~@{text "= bool"}
    1.39 +  determines whether the printed version of qualified names should be
    1.40 +  made sufficiently long to avoid overlap with names declared further
    1.41 +  back.  Set to @{text false} for more concise output.
    1.42  
    1.43 -  \item @{text "eta_contract = bool"} prints terms in @{text
    1.44 -  \<eta>}-contracted form.
    1.45 +  \item @{antiquotation_option_def eta_contract}~@{text "= bool"}
    1.46 +  prints terms in @{text \<eta>}-contracted form.
    1.47  
    1.48 -  \item @{text "display = bool"} indicates if the text is to be output
    1.49 -  as multi-line ``display material'', rather than a small piece of
    1.50 -  text without line breaks (which is the default).
    1.51 +  \item @{antiquotation_option_def display}~@{text "= bool"} indicates
    1.52 +  if the text is to be output as multi-line ``display material'',
    1.53 +  rather than a small piece of text without line breaks (which is the
    1.54 +  default).
    1.55  
    1.56    In this mode the embedded entities are printed in the same style as
    1.57    the main theory text.
    1.58  
    1.59 -  \item @{text "break = bool"} controls line breaks in non-display
    1.60 -  material.
    1.61 +  \item @{antiquotation_option_def break}~@{text "= bool"} controls
    1.62 +  line breaks in non-display material.
    1.63  
    1.64 -  \item @{text "quotes = bool"} indicates if the output should be
    1.65 -  enclosed in double quotes.
    1.66 +  \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates
    1.67 +  if the output should be enclosed in double quotes.
    1.68  
    1.69 -  \item @{text "mode = name"} adds @{text name} to the print mode to
    1.70 -  be used for presentation (see also \cite{isabelle-ref}).  Note that
    1.71 -  the standard setup for {\LaTeX} output is already present by
    1.72 -  default, including the modes @{text latex} and @{text xsymbols}.
    1.73 +  \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text
    1.74 +  name} to the print mode to be used for presentation.  Note that the
    1.75 +  standard setup for {\LaTeX} output is already present by default,
    1.76 +  including the modes @{text latex} and @{text xsymbols}.
    1.77  
    1.78 -  \item @{text "margin = nat"} and @{text "indent = nat"} change the
    1.79 -  margin or indentation for pretty printing of display material.
    1.80 -
    1.81 -  \item @{text "goals_limit = nat"} determines the maximum number of
    1.82 -  goals to be printed (for goal-based antiquotation).
    1.83 +  \item @{antiquotation_option_def margin}~@{text "= nat"} and
    1.84 +  @{antiquotation_option_def indent}~@{text "= nat"} change the margin
    1.85 +  or indentation for pretty printing of display material.
    1.86  
    1.87 -  \item @{text "locale = name"} specifies an alternative locale
    1.88 -  context used for evaluating and printing the subsequent argument.
    1.89 +  \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
    1.90 +  determines the maximum number of goals to be printed (for goal-based
    1.91 +  antiquotation).
    1.92  
    1.93 -  \item @{text "source = bool"} prints the original source text of the
    1.94 -  antiquotation arguments, rather than its internal representation.
    1.95 -  Note that formal checking of @{antiquotation "thm"}, @{antiquotation
    1.96 -  "term"}, etc. is still enabled; use the @{antiquotation "text"}
    1.97 -  antiquotation for unchecked output.
    1.98 +  \item @{antiquotation_option_def source}~@{text "= bool"} prints the
    1.99 +  original source text of the antiquotation arguments, rather than its
   1.100 +  internal representation.  Note that formal checking of
   1.101 +  @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
   1.102 +  enabled; use the @{antiquotation "text"} antiquotation for unchecked
   1.103 +  output.
   1.104  
   1.105    Regular @{text "term"} and @{text "typ"} antiquotations with @{text
   1.106    "source = false"} involve a full round-trip from the original source
   1.107 @@ -380,9 +382,10 @@
   1.108    not under direct control of the author, it may even fluctuate a bit
   1.109    as the underlying theory is changed later on.
   1.110  
   1.111 -  In contrast, @{text "source = true"} admits direct printing of the
   1.112 -  given source text, with the desirable well-formedness check in the
   1.113 -  background, but without modification of the printed text.
   1.114 +  In contrast, @{antiquotation_option_def source}~@{text "= true"}
   1.115 +  admits direct printing of the given source text, with the desirable
   1.116 +  well-formedness check in the background, but without modification of
   1.117 +  the printed text.
   1.118  
   1.119    \end{description}
   1.120  
     2.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Mon Mar 09 21:23:40 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Mon Mar 09 21:25:33 2009 +0100
     2.3 @@ -78,13 +78,14 @@
     2.4    into all goals of the proof state.  Note that current facts
     2.5    indicated for forward chaining are ignored.
     2.6  
     2.7 -  \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1
     2.8 -  \<dots> a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the
     2.9 -  basic @{method rule} method (see \secref{sec:pure-meth-att}), but
    2.10 -  apply rules by elim-resolution, destruct-resolution, and
    2.11 -  forward-resolution, respectively \cite{isabelle-ref}.  The optional
    2.12 -  natural number argument (default 0) specifies additional assumption
    2.13 -  steps to be performed here.
    2.14 +  \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
    2.15 +  drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
    2.16 +  "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
    2.17 +  method (see \secref{sec:pure-meth-att}), but apply rules by
    2.18 +  elim-resolution, destruct-resolution, and forward-resolution,
    2.19 +  respectively \cite{isabelle-implementation}.  The optional natural
    2.20 +  number argument (default 0) specifies additional assumption steps to
    2.21 +  be performed here.
    2.22  
    2.23    Note that these methods are improper ones, mainly serving for
    2.24    experimentation and tactic script emulation.  Different modes of
    2.25 @@ -143,7 +144,7 @@
    2.26    specified); the @{attribute COMP} version skips the automatic
    2.27    lifting process that is normally intended (cf.\ @{ML [source=false]
    2.28    "op RS"} and @{ML [source=false] "op COMP"} in
    2.29 -  \cite[\S5]{isabelle-ref}).
    2.30 +  \cite{isabelle-implementation}).
    2.31    
    2.32    \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
    2.33    folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
    2.34 @@ -304,26 +305,26 @@
    2.35  
    2.36    \item @{method rule_tac} etc. do resolution of rules with explicit
    2.37    instantiation.  This works the same way as the ML tactics @{ML
    2.38 -  res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
    2.39 +  res_inst_tac} etc. (see \cite{isabelle-implementation})
    2.40  
    2.41    Multiple rules may be only given if there is no instantiation; then
    2.42    @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
    2.43 -  \cite[\S3]{isabelle-ref}).
    2.44 +  \cite{isabelle-implementation}).
    2.45  
    2.46    \item @{method cut_tac} inserts facts into the proof state as
    2.47    assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
    2.48 -  \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
    2.49 +  \cite{isabelle-implementation}.  Note that the scope of schematic
    2.50    variables is spread over the main goal statement.  Instantiations
    2.51    may be given as well, see also ML tactic @{ML cut_inst_tac} in
    2.52 -  \cite[\S3]{isabelle-ref}.
    2.53 +  \cite{isabelle-implementation}.
    2.54  
    2.55    \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
    2.56    from a subgoal; note that @{text \<phi>} may contain schematic variables.
    2.57 -  See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
    2.58 +  See also @{ML thin_tac} in \cite{isabelle-implementation}.
    2.59  
    2.60    \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
    2.61    assumption to a subgoal.  See also @{ML subgoal_tac} and @{ML
    2.62 -  subgoals_tac} in \cite[\S3]{isabelle-ref}.
    2.63 +  subgoals_tac} in \cite{isabelle-implementation}.
    2.64  
    2.65    \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
    2.66    goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
    2.67 @@ -333,7 +334,7 @@
    2.68    goal by @{text n} positions: from right to left if @{text n} is
    2.69    positive, and from left to right if @{text n} is negative; the
    2.70    default value is 1.  See also @{ML rotate_tac} in
    2.71 -  \cite[\S3]{isabelle-ref}.
    2.72 +  \cite{isabelle-implementation}.
    2.73  
    2.74    \item @{method tactic}~@{text "text"} produces a proof method from
    2.75    any ML text of type @{ML_type tactic}.  Apart from the usual ML
    2.76 @@ -400,13 +401,13 @@
    2.77    By default the Simplifier methods take local assumptions fully into
    2.78    account, using equational assumptions in the subsequent
    2.79    normalization process, or simplifying assumptions themselves (cf.\
    2.80 -  @{ML asm_full_simp_tac} in \cite[\S10]{isabelle-ref}).  In
    2.81 -  structured proofs this is usually quite well behaved in practice:
    2.82 -  just the local premises of the actual goal are involved, additional
    2.83 -  facts may be inserted via explicit forward-chaining (via @{command
    2.84 -  "then"}, @{command "from"}, @{command "using"} etc.).  The full
    2.85 -  context of premises is only included if the ``@{text "!"}'' (bang)
    2.86 -  argument is given, which should be used with some care, though.
    2.87 +  @{ML asm_full_simp_tac} in \cite{isabelle-ref}).  In structured
    2.88 +  proofs this is usually quite well behaved in practice: just the
    2.89 +  local premises of the actual goal are involved, additional facts may
    2.90 +  be inserted via explicit forward-chaining (via @{command "then"},
    2.91 +  @{command "from"}, @{command "using"} etc.).  The full context of
    2.92 +  premises is only included if the ``@{text "!"}'' (bang) argument is
    2.93 +  given, which should be used with some care, though.
    2.94  
    2.95    Additional Simplifier options may be specified to tune the behavior
    2.96    further (mostly for unstructured scripts with many accidental local
    2.97 @@ -615,14 +616,14 @@
    2.98    \begin{description}
    2.99  
   2.100    \item @{method blast} refers to the classical tableau prover (see
   2.101 -  @{ML blast_tac} in \cite[\S11]{isabelle-ref}).  The optional
   2.102 -  argument specifies a user-supplied search bound (default 20).
   2.103 +  @{ML blast_tac} in \cite{isabelle-ref}).  The optional argument
   2.104 +  specifies a user-supplied search bound (default 20).
   2.105  
   2.106    \item @{method fast}, @{method slow}, @{method best}, @{method
   2.107    safe}, and @{method clarify} refer to the generic classical
   2.108    reasoner.  See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
   2.109 -  safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for
   2.110 -  more information.
   2.111 +  safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
   2.112 +  information.
   2.113  
   2.114    \end{description}
   2.115  
   2.116 @@ -667,8 +668,8 @@
   2.117    to Isabelle's combined simplification and classical reasoning
   2.118    tactics.  These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
   2.119    clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
   2.120 -  added as wrapper, see \cite[\S11]{isabelle-ref} for more
   2.121 -  information.  The modifier arguments correspond to those given in
   2.122 +  added as wrapper, see \cite{isabelle-ref} for more information.  The
   2.123 +  modifier arguments correspond to those given in
   2.124    \secref{sec:simplifier} and \secref{sec:classical}.  Just note that
   2.125    the ones related to the Simplifier are prefixed by \railtterm{simp}
   2.126    here.
     3.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Mar 09 21:23:40 2009 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Mar 09 21:25:33 2009 +0100
     3.3 @@ -799,8 +799,8 @@
     3.4    translations functions may refer to specific theory declarations or
     3.5    auxiliary proof data.
     3.6  
     3.7 -  See also \cite[\S8]{isabelle-ref} for more information on the
     3.8 -  general concept of syntax transformations in Isabelle.
     3.9 +  See also \cite{isabelle-ref} for more information on the general
    3.10 +  concept of syntax transformations in Isabelle.
    3.11  
    3.12  %FIXME proper antiquotations
    3.13  \begin{ttbox}
     4.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Mar 09 21:23:40 2009 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Mar 09 21:25:33 2009 +0100
     4.3 @@ -335,59 +335,62 @@
     4.4  
     4.5    \begin{description}
     4.6  
     4.7 -  \item \isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}
     4.8 -  control printing of explicit type and sort constraints.
     4.9 +  \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
    4.10 +  \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
    4.11 +  printing of explicit type and sort constraints.
    4.12  
    4.13 -  \item \isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}} controls printing of implicit
    4.14 -  structures.
    4.15 +  \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}}
    4.16 +  controls printing of implicit structures.
    4.17  
    4.18 -  \item \isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
    4.19 -  constants etc.\ to be printed in their fully qualified internal
    4.20 -  form.
    4.21 +  \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
    4.22 +  names of types and constants etc.\ to be printed in their fully
    4.23 +  qualified internal form.
    4.24  
    4.25 -  \item \isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
    4.26 -  constants etc.\ to be printed unqualified.  Note that internalizing
    4.27 -  the output again in the current context may well yield a different
    4.28 -  result.
    4.29 +  \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}}
    4.30 +  forces names of types and constants etc.\ to be printed unqualified.
    4.31 +  Note that internalizing the output again in the current context may
    4.32 +  well yield a different result.
    4.33  
    4.34 -  \item \isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} determines whether the printed
    4.35 -  version of qualified names should be made sufficiently long to avoid
    4.36 -  overlap with names declared further back.  Set to \isa{false} for
    4.37 -  more concise output.
    4.38 +  \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}}
    4.39 +  determines whether the printed version of qualified names should be
    4.40 +  made sufficiently long to avoid overlap with names declared further
    4.41 +  back.  Set to \isa{false} for more concise output.
    4.42  
    4.43 -  \item \isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}} prints terms in \isa{{\isasymeta}}-contracted form.
    4.44 +  \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}}
    4.45 +  prints terms in \isa{{\isasymeta}}-contracted form.
    4.46  
    4.47 -  \item \isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the text is to be output
    4.48 -  as multi-line ``display material'', rather than a small piece of
    4.49 -  text without line breaks (which is the default).
    4.50 +  \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
    4.51 +  if the text is to be output as multi-line ``display material'',
    4.52 +  rather than a small piece of text without line breaks (which is the
    4.53 +  default).
    4.54  
    4.55    In this mode the embedded entities are printed in the same style as
    4.56    the main theory text.
    4.57  
    4.58 -  \item \isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}} controls line breaks in non-display
    4.59 -  material.
    4.60 +  \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
    4.61 +  line breaks in non-display material.
    4.62  
    4.63 -  \item \isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the output should be
    4.64 -  enclosed in double quotes.
    4.65 +  \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
    4.66 +  if the output should be enclosed in double quotes.
    4.67  
    4.68 -  \item \isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to
    4.69 -  be used for presentation (see also \cite{isabelle-ref}).  Note that
    4.70 -  the standard setup for {\LaTeX} output is already present by
    4.71 -  default, including the modes \isa{latex} and \isa{xsymbols}.
    4.72 +  \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
    4.73 +  standard setup for {\LaTeX} output is already present by default,
    4.74 +  including the modes \isa{latex} and \isa{xsymbols}.
    4.75  
    4.76 -  \item \isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}} change the
    4.77 -  margin or indentation for pretty printing of display material.
    4.78 -
    4.79 -  \item \isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}} determines the maximum number of
    4.80 -  goals to be printed (for goal-based antiquotation).
    4.81 +  \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
    4.82 +  \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
    4.83 +  or indentation for pretty printing of display material.
    4.84  
    4.85 -  \item \isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}} specifies an alternative locale
    4.86 -  context used for evaluating and printing the subsequent argument.
    4.87 +  \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}}
    4.88 +  determines the maximum number of goals to be printed (for goal-based
    4.89 +  antiquotation).
    4.90  
    4.91 -  \item \isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}} prints the original source text of the
    4.92 -  antiquotation arguments, rather than its internal representation.
    4.93 -  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}}}
    4.94 -  antiquotation for unchecked output.
    4.95 +  \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
    4.96 +  original source text of the antiquotation arguments, rather than its
    4.97 +  internal representation.  Note that formal checking of
    4.98 +  \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
    4.99 +  enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
   4.100 +  output.
   4.101  
   4.102    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
   4.103    to an internalized logical entity back to a source form, according
   4.104 @@ -395,9 +398,10 @@
   4.105    not under direct control of the author, it may even fluctuate a bit
   4.106    as the underlying theory is changed later on.
   4.107  
   4.108 -  In contrast, \isa{{\isachardoublequote}source\ {\isacharequal}\ true{\isachardoublequote}} admits direct printing of the
   4.109 -  given source text, with the desirable well-formedness check in the
   4.110 -  background, but without modification of the printed text.
   4.111 +  In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
   4.112 +  admits direct printing of the given source text, with the desirable
   4.113 +  well-formedness check in the background, but without modification of
   4.114 +  the printed text.
   4.115  
   4.116    \end{description}
   4.117  
     5.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Mar 09 21:23:40 2009 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon Mar 09 21:25:33 2009 +0100
     5.3 @@ -99,12 +99,12 @@
     5.4    into all goals of the proof state.  Note that current facts
     5.5    indicated for forward chaining are ignored.
     5.6  
     5.7 -  \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
     5.8 -  basic \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see \secref{sec:pure-meth-att}), but
     5.9 -  apply rules by elim-resolution, destruct-resolution, and
    5.10 -  forward-resolution, respectively \cite{isabelle-ref}.  The optional
    5.11 -  natural number argument (default 0) specifies additional assumption
    5.12 -  steps to be performed here.
    5.13 +  \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}}}
    5.14 +  method (see \secref{sec:pure-meth-att}), but apply rules by
    5.15 +  elim-resolution, destruct-resolution, and forward-resolution,
    5.16 +  respectively \cite{isabelle-implementation}.  The optional natural
    5.17 +  number argument (default 0) specifies additional assumption steps to
    5.18 +  be performed here.
    5.19  
    5.20    Note that these methods are improper ones, mainly serving for
    5.21    experimentation and tactic script emulation.  Different modes of
    5.22 @@ -161,7 +161,7 @@
    5.23    first premise of \isa{a} (an alternative position may be also
    5.24    specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
    5.25    lifting process that is normally intended (cf.\ \verb|op RS| and \verb|op COMP| in
    5.26 -  \cite[\S5]{isabelle-ref}).
    5.27 +  \cite{isabelle-implementation}).
    5.28    
    5.29    \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
    5.30    definitions throughout a rule.
    5.31 @@ -321,25 +321,25 @@
    5.32  \begin{description}
    5.33  
    5.34    \item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc. do resolution of rules with explicit
    5.35 -  instantiation.  This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref})
    5.36 +  instantiation.  This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
    5.37  
    5.38    Multiple rules may be only given if there is no instantiation; then
    5.39    \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
    5.40 -  \cite[\S3]{isabelle-ref}).
    5.41 +  \cite{isabelle-implementation}).
    5.42  
    5.43    \item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}} inserts facts into the proof state as
    5.44    assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
    5.45 -  \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
    5.46 +  \cite{isabelle-implementation}.  Note that the scope of schematic
    5.47    variables is spread over the main goal statement.  Instantiations
    5.48    may be given as well, see also ML tactic \verb|cut_inst_tac| in
    5.49 -  \cite[\S3]{isabelle-ref}.
    5.50 +  \cite{isabelle-implementation}.
    5.51  
    5.52    \item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} deletes the specified assumption
    5.53    from a subgoal; note that \isa{{\isasymphi}} may contain schematic variables.
    5.54 -  See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
    5.55 +  See also \verb|thin_tac| in \cite{isabelle-implementation}.
    5.56  
    5.57    \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} adds \isa{{\isasymphi}} as an
    5.58 -  assumption to a subgoal.  See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
    5.59 +  assumption to a subgoal.  See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
    5.60  
    5.61    \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
    5.62    goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the
    5.63 @@ -349,7 +349,7 @@
    5.64    goal by \isa{n} positions: from right to left if \isa{n} is
    5.65    positive, and from left to right if \isa{n} is negative; the
    5.66    default value is 1.  See also \verb|rotate_tac| in
    5.67 -  \cite[\S3]{isabelle-ref}.
    5.68 +  \cite{isabelle-implementation}.
    5.69  
    5.70    \item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} produces a proof method from
    5.71    any ML text of type \verb|tactic|.  Apart from the usual ML
    5.72 @@ -420,12 +420,13 @@
    5.73    By default the Simplifier methods take local assumptions fully into
    5.74    account, using equational assumptions in the subsequent
    5.75    normalization process, or simplifying assumptions themselves (cf.\
    5.76 -  \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}).  In
    5.77 -  structured proofs this is usually quite well behaved in practice:
    5.78 -  just the local premises of the actual goal are involved, additional
    5.79 -  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
    5.80 -  context of premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang)
    5.81 -  argument is given, which should be used with some care, though.
    5.82 +  \verb|asm_full_simp_tac| in \cite{isabelle-ref}).  In structured
    5.83 +  proofs this is usually quite well behaved in practice: just the
    5.84 +  local premises of the actual goal are involved, additional facts may
    5.85 +  be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
    5.86 +  \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).  The full context of
    5.87 +  premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
    5.88 +  given, which should be used with some care, though.
    5.89  
    5.90    Additional Simplifier options may be specified to tune the behavior
    5.91    further (mostly for unstructured scripts with many accidental local
    5.92 @@ -637,12 +638,12 @@
    5.93    \begin{description}
    5.94  
    5.95    \item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
    5.96 -  \verb|blast_tac| in \cite[\S11]{isabelle-ref}).  The optional
    5.97 -  argument specifies a user-supplied search bound (default 20).
    5.98 +  \verb|blast_tac| in \cite{isabelle-ref}).  The optional argument
    5.99 +  specifies a user-supplied search bound (default 20).
   5.100  
   5.101    \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
   5.102 -  reasoner.  See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite[\S11]{isabelle-ref} for
   5.103 -  more information.
   5.104 +  reasoner.  See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
   5.105 +  information.
   5.106  
   5.107    \end{description}
   5.108  
   5.109 @@ -686,8 +687,8 @@
   5.110    \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
   5.111    to Isabelle's combined simplification and classical reasoning
   5.112    tactics.  These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
   5.113 -  added as wrapper, see \cite[\S11]{isabelle-ref} for more
   5.114 -  information.  The modifier arguments correspond to those given in
   5.115 +  added as wrapper, see \cite{isabelle-ref} for more information.  The
   5.116 +  modifier arguments correspond to those given in
   5.117    \secref{sec:simplifier} and \secref{sec:classical}.  Just note that
   5.118    the ones related to the Simplifier are prefixed by \railtterm{simp}
   5.119    here.
     6.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Mar 09 21:23:40 2009 +0100
     6.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Mar 09 21:25:33 2009 +0100
     6.3 @@ -819,8 +819,8 @@
     6.4    translations functions may refer to specific theory declarations or
     6.5    auxiliary proof data.
     6.6  
     6.7 -  See also \cite[\S8]{isabelle-ref} for more information on the
     6.8 -  general concept of syntax transformations in Isabelle.
     6.9 +  See also \cite{isabelle-ref} for more information on the general
    6.10 +  concept of syntax transformations in Isabelle.
    6.11  
    6.12  %FIXME proper antiquotations
    6.13  \begin{ttbox}