updated configuration options -- no ML here;
authorwenzelm
Tue May 03 16:00:29 2011 +0200 (2011-05-03)
changeset 42655eb95e2f3b218
parent 42654 b1a051891ec4
child 42656 89132fbd852a
updated configuration options -- no ML here;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Tue May 03 15:37:17 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Tue May 03 16:00:29 2011 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  chapter {* Generic tools and packages \label{ch:gen-tools} *}
     1.6  
     1.7 -section {* Configuration options *}
     1.8 +section {* Configuration options \label{sec:config} *}
     1.9  
    1.10  text {* Isabelle/Pure maintains a record of named configuration
    1.11    options within the theory or proof context, with values of type
    1.12 @@ -14,9 +14,18 @@
    1.13    are easily avoided.  The user may change the value of a
    1.14    configuration option by means of an associated attribute of the same
    1.15    name.  This form of context declaration works particularly well with
    1.16 -  commands such as @{command "declare"} or @{command "using"}.
    1.17 +  commands such as @{command "declare"} or @{command "using"} like
    1.18 +  this:
    1.19 +*}
    1.20 +
    1.21 +declare [[show_main_goal = false]]
    1.22  
    1.23 -  For historical reasons, some tools cannot take the full proof
    1.24 +notepad
    1.25 +begin
    1.26 +  note [[show_main_goal = true]]
    1.27 +end
    1.28 +
    1.29 +text {* For historical reasons, some tools cannot take the full proof
    1.30    context into account and merely refer to the background theory.
    1.31    This is accommodated by configuration options being declared as
    1.32    ``global'', which may not be changed within a local context.
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue May 03 15:37:17 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue May 03 16:00:29 2011 +0200
     2.3 @@ -94,70 +94,64 @@
     2.4  subsection {* Details of printed content *}
     2.5  
     2.6  text {*
     2.7 -  \begin{mldecls} 
     2.8 -    @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
     2.9 -    @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
    2.10 -    @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
    2.11 -    @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
    2.12 -    @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
    2.13 -    @{index_ML Name_Space.long_names: "bool Config.T"} & default @{ML false} \\
    2.14 -    @{index_ML Name_Space.short_names: "bool Config.T"} & default @{ML false} \\
    2.15 -    @{index_ML Name_Space.unique_names: "bool Config.T"} & default @{ML true} \\
    2.16 -    @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
    2.17 -    @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
    2.18 -    @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
    2.19 -    @{index_ML show_hyps: "bool Config.T"} & default @{ML false} \\
    2.20 -    @{index_ML show_tags: "bool Config.T"} & default @{ML false} \\
    2.21 -    @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
    2.22 -  \end{mldecls}
    2.23 +  \begin{tabular}{rcll}
    2.24 +    @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
    2.25 +    @{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
    2.26 +    @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
    2.27 +    @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
    2.28 +    @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
    2.29 +    @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\
    2.30 +    @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\
    2.31 +    @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\
    2.32 +    @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
    2.33 +    @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
    2.34 +    @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
    2.35 +    @{attribute_def show_hyps} & : & @{text attribute} & default @{text false} \\
    2.36 +    @{attribute_def show_tags} & : & @{text attribute} & default @{text false} \\
    2.37 +    @{attribute_def show_question_marks} & : & @{text attribute} & default @{text true} \\
    2.38 +  \end{tabular}
    2.39 +  \medskip
    2.40  
    2.41 -  These global ML variables control the detail of information that is
    2.42 -  displayed for types, terms, theorems, goals etc.
    2.43 -
    2.44 -  In interactive sessions, the user interface usually manages these
    2.45 -  global parameters of the Isabelle process, even with some concept of
    2.46 -  persistence.  Nonetheless it is occasionally useful to manipulate ML
    2.47 -  variables directly, e.g.\ using @{command "ML_val"} or @{command
    2.48 -  "ML_command"}.
    2.49 -
    2.50 -  Batch-mode logic sessions may be configured by putting appropriate
    2.51 -  ML text directly into the @{verbatim ROOT.ML} file.
    2.52 +  These configuration options control the detail of information that
    2.53 +  is displayed for types, terms, theorems, goals etc.  See also
    2.54 +  \secref{sec:config}.
    2.55  
    2.56    \begin{description}
    2.57  
    2.58 -  \item @{ML show_types} and @{ML show_sorts} control printing of type
    2.59 -  constraints for term variables, and sort constraints for type
    2.60 -  variables.  By default, neither of these are shown in output.  If
    2.61 -  @{ML show_sorts} is set to @{ML true}, types are always shown as
    2.62 -  well.
    2.63 +  \item @{attribute show_types} and @{attribute show_sorts} control
    2.64 +  printing of type constraints for term variables, and sort
    2.65 +  constraints for type variables.  By default, neither of these are
    2.66 +  shown in output.  If @{attribute show_sorts} is enabled, types are
    2.67 +  always shown as well.
    2.68  
    2.69    Note that displaying types and sorts may explain why a polymorphic
    2.70    inference rule fails to resolve with some goal, or why a rewrite
    2.71    rule does not apply as expected.
    2.72  
    2.73 -  \item @{ML show_consts} controls printing of types of constants when
    2.74 -  displaying a goal state.
    2.75 +  \item @{attribute show_consts} controls printing of types of
    2.76 +  constants when displaying a goal state.
    2.77  
    2.78    Note that the output can be enormous, because polymorphic constants
    2.79    often occur at several different type instances.
    2.80  
    2.81 -  \item @{ML show_abbrevs} controls folding of constant abbreviations.
    2.82 +  \item @{attribute show_abbrevs} controls folding of constant
    2.83 +  abbreviations.
    2.84  
    2.85 -  \item @{ML show_brackets} controls bracketing in pretty printed
    2.86 -  output.  If set to @{ML true}, all sub-expressions of the pretty
    2.87 +  \item @{attribute show_brackets} controls bracketing in pretty
    2.88 +  printed output.  If enabled, all sub-expressions of the pretty
    2.89    printing tree will be parenthesized, even if this produces malformed
    2.90    term syntax!  This crude way of showing the internal structure of
    2.91    pretty printed entities may occasionally help to diagnose problems
    2.92    with operator priorities, for example.
    2.93  
    2.94 -  \item @{ML Name_Space.long_names}, @{ML Name_Space.short_names}, and
    2.95 -  @{ML Name_Space.unique_names} control the way of printing fully
    2.96 +  \item @{attribute long_names}, @{attribute short_names}, and
    2.97 +  @{attribute unique_names} control the way of printing fully
    2.98    qualified internal names in external form.  See also
    2.99    \secref{sec:antiq} for the document antiquotation options of the
   2.100    same names.
   2.101  
   2.102 -  \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
   2.103 -  terms.
   2.104 +  \item @{attribute eta_contract} controls @{text "\<eta>"}-contracted
   2.105 +  printing of terms.
   2.106  
   2.107    The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
   2.108    provided @{text x} is not free in @{text f}.  It asserts
   2.109 @@ -167,7 +161,7 @@
   2.110    F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
   2.111    "\<lambda>h. F (\<lambda>x. h x)"}.
   2.112  
   2.113 -  Setting @{ML eta_contract} makes Isabelle perform @{text
   2.114 +  Enabling @{attribute eta_contract} makes Isabelle perform @{text
   2.115    \<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
   2.116    appears simply as @{text F}.
   2.117  
   2.118 @@ -176,33 +170,34 @@
   2.119    rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
   2.120    might look at terms more discretely.
   2.121  
   2.122 -  \item @{ML Goal_Display.goals_limit} controls the maximum number of
   2.123 +  \item @{attribute goals_limit} controls the maximum number of
   2.124    subgoals to be shown in goal output.
   2.125  
   2.126 -  \item @{ML Goal_Display.show_main_goal} controls whether the main
   2.127 -  result to be proven should be displayed.  This information might be
   2.128 +  \item @{attribute show_main_goal} controls whether the main result
   2.129 +  to be proven should be displayed.  This information might be
   2.130    relevant for schematic goals, to inspect the current claim that has
   2.131    been synthesized so far.
   2.132  
   2.133 -  \item @{ML show_hyps} controls printing of implicit hypotheses of
   2.134 -  local facts.  Normally, only those hypotheses are displayed that are
   2.135 -  \emph{not} covered by the assumptions of the current context: this
   2.136 -  situation indicates a fault in some tool being used.
   2.137 +  \item @{attribute show_hyps} controls printing of implicit
   2.138 +  hypotheses of local facts.  Normally, only those hypotheses are
   2.139 +  displayed that are \emph{not} covered by the assumptions of the
   2.140 +  current context: this situation indicates a fault in some tool being
   2.141 +  used.
   2.142  
   2.143 -  By setting @{ML show_hyps} to @{ML true}, output of \emph{all}
   2.144 -  hypotheses can be enforced, which is occasionally useful for
   2.145 -  diagnostic purposes.
   2.146 +  By enabling @{attribute show_hyps}, output of \emph{all} hypotheses
   2.147 +  can be enforced, which is occasionally useful for diagnostic
   2.148 +  purposes.
   2.149  
   2.150 -  \item @{ML show_tags} controls printing of extra annotations within
   2.151 -  theorems, such as internal position information, or the case names
   2.152 -  being attached by the attribute @{attribute case_names}.
   2.153 +  \item @{attribute show_tags} controls printing of extra annotations
   2.154 +  within theorems, such as internal position information, or the case
   2.155 +  names being attached by the attribute @{attribute case_names}.
   2.156  
   2.157    Note that the @{attribute tagged} and @{attribute untagged}
   2.158    attributes provide low-level access to the collection of tags
   2.159    associated with a theorem.
   2.160  
   2.161 -  \item @{ML show_question_marks} controls printing of question marks
   2.162 -  for schematic variables, such as @{text ?x}.  Only the leading
   2.163 +  \item @{attribute show_question_marks} controls printing of question
   2.164 +  marks for schematic variables, such as @{text ?x}.  Only the leading
   2.165    question mark is affected, the remaining text is unchanged
   2.166    (including proper markup for schematic variables that might be
   2.167    relevant for user interfaces).
     3.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 03 15:37:17 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 03 16:00:29 2011 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsection{Configuration options%
     3.8 +\isamarkupsection{Configuration options \label{sec:config}%
     3.9  }
    3.10  \isamarkuptrue%
    3.11  %
    3.12 @@ -34,9 +34,35 @@
    3.13    are easily avoided.  The user may change the value of a
    3.14    configuration option by means of an associated attribute of the same
    3.15    name.  This form of context declaration works particularly well with
    3.16 -  commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
    3.17 -
    3.18 -  For historical reasons, some tools cannot take the full proof
    3.19 +  commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} like
    3.20 +  this:%
    3.21 +\end{isamarkuptext}%
    3.22 +\isamarkuptrue%
    3.23 +\isacommand{declare}\isamarkupfalse%
    3.24 +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
    3.25 +\isanewline
    3.26 +\isacommand{notepad}\isamarkupfalse%
    3.27 +\isanewline
    3.28 +\isakeyword{begin}\isanewline
    3.29 +%
    3.30 +\isadelimproof
    3.31 +\ \ %
    3.32 +\endisadelimproof
    3.33 +%
    3.34 +\isatagproof
    3.35 +\isacommand{note}\isamarkupfalse%
    3.36 +\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%
    3.37 +\endisatagproof
    3.38 +{\isafoldproof}%
    3.39 +%
    3.40 +\isadelimproof
    3.41 +\isanewline
    3.42 +%
    3.43 +\endisadelimproof
    3.44 +\isacommand{end}\isamarkupfalse%
    3.45 +%
    3.46 +\begin{isamarkuptext}%
    3.47 +For historical reasons, some tools cannot take the full proof
    3.48    context into account and merely refer to the background theory.
    3.49    This is accommodated by configuration options being declared as
    3.50    ``global'', which may not be changed within a local context.
     4.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 15:37:17 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 16:00:29 2011 +0200
     4.3 @@ -169,76 +169,71 @@
     4.4  \isamarkuptrue%
     4.5  %
     4.6  \begin{isamarkuptext}%
     4.7 -\begin{mldecls} 
     4.8 -    \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
     4.9 -    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
    4.10 -    \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
    4.11 -    \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
    4.12 -    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
    4.13 -    \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\
    4.14 -    \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\
    4.15 -    \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\
    4.16 -    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
    4.17 -    \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
    4.18 -    \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
    4.19 -    \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\
    4.20 -    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\
    4.21 -    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
    4.22 -  \end{mldecls}
    4.23 +\begin{tabular}{rcll}
    4.24 +    \indexdef{}{attribute}{show\_types}\hypertarget{attribute.show-types}{\hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}}} & : & \isa{attribute} & default \isa{false} \\
    4.25 +    \indexdef{}{attribute}{show\_sorts}\hypertarget{attribute.show-sorts}{\hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}}} & : & \isa{attribute} & default \isa{false} \\
    4.26 +    \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
    4.27 +    \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
    4.28 +    \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
    4.29 +    \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
    4.30 +    \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
    4.31 +    \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\
    4.32 +    \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
    4.33 +    \indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
    4.34 +    \indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\
    4.35 +    \indexdef{}{attribute}{show\_hyps}\hypertarget{attribute.show-hyps}{\hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}} & : & \isa{attribute} & default \isa{false} \\
    4.36 +    \indexdef{}{attribute}{show\_tags}\hypertarget{attribute.show-tags}{\hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}}} & : & \isa{attribute} & default \isa{false} \\
    4.37 +    \indexdef{}{attribute}{show\_question\_marks}\hypertarget{attribute.show-question-marks}{\hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}}} & : & \isa{attribute} & default \isa{true} \\
    4.38 +  \end{tabular}
    4.39 +  \medskip
    4.40  
    4.41 -  These global ML variables control the detail of information that is
    4.42 -  displayed for types, terms, theorems, goals etc.
    4.43 -
    4.44 -  In interactive sessions, the user interface usually manages these
    4.45 -  global parameters of the Isabelle process, even with some concept of
    4.46 -  persistence.  Nonetheless it is occasionally useful to manipulate ML
    4.47 -  variables directly, e.g.\ using \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}.
    4.48 -
    4.49 -  Batch-mode logic sessions may be configured by putting appropriate
    4.50 -  ML text directly into the \verb|ROOT.ML| file.
    4.51 +  These configuration options control the detail of information that
    4.52 +  is displayed for types, terms, theorems, goals etc.  See also
    4.53 +  \secref{sec:config}.
    4.54  
    4.55    \begin{description}
    4.56  
    4.57 -  \item \verb|show_types| and \verb|show_sorts| control printing of type
    4.58 -  constraints for term variables, and sort constraints for type
    4.59 -  variables.  By default, neither of these are shown in output.  If
    4.60 -  \verb|show_sorts| is set to \verb|true|, types are always shown as
    4.61 -  well.
    4.62 +  \item \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} and \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} control
    4.63 +  printing of type constraints for term variables, and sort
    4.64 +  constraints for type variables.  By default, neither of these are
    4.65 +  shown in output.  If \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} is enabled, types are
    4.66 +  always shown as well.
    4.67  
    4.68    Note that displaying types and sorts may explain why a polymorphic
    4.69    inference rule fails to resolve with some goal, or why a rewrite
    4.70    rule does not apply as expected.
    4.71  
    4.72 -  \item \verb|show_consts| controls printing of types of constants when
    4.73 -  displaying a goal state.
    4.74 +  \item \hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}} controls printing of types of
    4.75 +  constants when displaying a goal state.
    4.76  
    4.77    Note that the output can be enormous, because polymorphic constants
    4.78    often occur at several different type instances.
    4.79  
    4.80 -  \item \verb|show_abbrevs| controls folding of constant abbreviations.
    4.81 +  \item \hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}} controls folding of constant
    4.82 +  abbreviations.
    4.83  
    4.84 -  \item \verb|show_brackets| controls bracketing in pretty printed
    4.85 -  output.  If set to \verb|true|, all sub-expressions of the pretty
    4.86 +  \item \hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}} controls bracketing in pretty
    4.87 +  printed output.  If enabled, all sub-expressions of the pretty
    4.88    printing tree will be parenthesized, even if this produces malformed
    4.89    term syntax!  This crude way of showing the internal structure of
    4.90    pretty printed entities may occasionally help to diagnose problems
    4.91    with operator priorities, for example.
    4.92  
    4.93 -  \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and
    4.94 -  \verb|Name_Space.unique_names| control the way of printing fully
    4.95 +  \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and
    4.96 +  \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully
    4.97    qualified internal names in external form.  See also
    4.98    \secref{sec:antiq} for the document antiquotation options of the
    4.99    same names.
   4.100  
   4.101 -  \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of
   4.102 -  terms.
   4.103 +  \item \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted
   4.104 +  printing of terms.
   4.105  
   4.106    The \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contraction law asserts \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ f{\isaliteral{22}{\isachardoublequote}}},
   4.107    provided \isa{x} is not free in \isa{f}.  It asserts
   4.108    \emph{extensionality} of functions: \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g\ x{\isaliteral{22}{\isachardoublequote}}} for all \isa{x}.  Higher-order unification frequently puts
   4.109    terms into a fully \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded form.  For example, if \isa{F} has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} then its expanded form is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
   4.110  
   4.111 -  Setting \verb|eta_contract| makes Isabelle perform \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contractions before printing, so that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
   4.112 +  Enabling \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} makes Isabelle perform \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contractions before printing, so that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
   4.113    appears simply as \isa{F}.
   4.114  
   4.115    Note that the distinction between a term and its \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded
   4.116 @@ -246,33 +241,34 @@
   4.117    rewriting operate modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-conversion, some other tools
   4.118    might look at terms more discretely.
   4.119  
   4.120 -  \item \verb|Goal_Display.goals_limit| controls the maximum number of
   4.121 +  \item \hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}} controls the maximum number of
   4.122    subgoals to be shown in goal output.
   4.123  
   4.124 -  \item \verb|Goal_Display.show_main_goal| controls whether the main
   4.125 -  result to be proven should be displayed.  This information might be
   4.126 +  \item \hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}} controls whether the main result
   4.127 +  to be proven should be displayed.  This information might be
   4.128    relevant for schematic goals, to inspect the current claim that has
   4.129    been synthesized so far.
   4.130  
   4.131 -  \item \verb|show_hyps| controls printing of implicit hypotheses of
   4.132 -  local facts.  Normally, only those hypotheses are displayed that are
   4.133 -  \emph{not} covered by the assumptions of the current context: this
   4.134 -  situation indicates a fault in some tool being used.
   4.135 +  \item \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}} controls printing of implicit
   4.136 +  hypotheses of local facts.  Normally, only those hypotheses are
   4.137 +  displayed that are \emph{not} covered by the assumptions of the
   4.138 +  current context: this situation indicates a fault in some tool being
   4.139 +  used.
   4.140  
   4.141 -  By setting \verb|show_hyps| to \verb|true|, output of \emph{all}
   4.142 -  hypotheses can be enforced, which is occasionally useful for
   4.143 -  diagnostic purposes.
   4.144 +  By enabling \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}, output of \emph{all} hypotheses
   4.145 +  can be enforced, which is occasionally useful for diagnostic
   4.146 +  purposes.
   4.147  
   4.148 -  \item \verb|show_tags| controls printing of extra annotations within
   4.149 -  theorems, such as internal position information, or the case names
   4.150 -  being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}.
   4.151 +  \item \hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}} controls printing of extra annotations
   4.152 +  within theorems, such as internal position information, or the case
   4.153 +  names being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}.
   4.154  
   4.155    Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}
   4.156    attributes provide low-level access to the collection of tags
   4.157    associated with a theorem.
   4.158  
   4.159 -  \item \verb|show_question_marks| controls printing of question marks
   4.160 -  for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}.  Only the leading
   4.161 +  \item \hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}} controls printing of question
   4.162 +  marks for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}.  Only the leading
   4.163    question mark is affected, the remaining text is unchanged
   4.164    (including proper markup for schematic variables that might be
   4.165    relevant for user interfaces).