--- a/doc-src/IsarRef/Thy/Generic.thy Tue May 03 15:37:17 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Tue May 03 16:00:29 2011 +0200
@@ -4,7 +4,7 @@
chapter {* Generic tools and packages \label{ch:gen-tools} *}
-section {* Configuration options *}
+section {* Configuration options \label{sec:config} *}
text {* Isabelle/Pure maintains a record of named configuration
options within the theory or proof context, with values of type
@@ -14,9 +14,18 @@
are easily avoided. The user may change the value of a
configuration option by means of an associated attribute of the same
name. This form of context declaration works particularly well with
- commands such as @{command "declare"} or @{command "using"}.
+ commands such as @{command "declare"} or @{command "using"} like
+ this:
+*}
+
+declare [[show_main_goal = false]]
- For historical reasons, some tools cannot take the full proof
+notepad
+begin
+ note [[show_main_goal = true]]
+end
+
+text {* For historical reasons, some tools cannot take the full proof
context into account and merely refer to the background theory.
This is accommodated by configuration options being declared as
``global'', which may not be changed within a local context.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 15:37:17 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue May 03 16:00:29 2011 +0200
@@ -94,70 +94,64 @@
subsection {* Details of printed content *}
text {*
- \begin{mldecls}
- @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
- @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
- @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
- @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
- @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
- @{index_ML Name_Space.long_names: "bool Config.T"} & default @{ML false} \\
- @{index_ML Name_Space.short_names: "bool Config.T"} & default @{ML false} \\
- @{index_ML Name_Space.unique_names: "bool Config.T"} & default @{ML true} \\
- @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
- @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
- @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
- @{index_ML show_hyps: "bool Config.T"} & default @{ML false} \\
- @{index_ML show_tags: "bool Config.T"} & default @{ML false} \\
- @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
- \end{mldecls}
+ \begin{tabular}{rcll}
+ @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
+ @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\
+ @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
+ @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
+ @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def show_hyps} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def show_tags} & : & @{text attribute} & default @{text false} \\
+ @{attribute_def show_question_marks} & : & @{text attribute} & default @{text true} \\
+ \end{tabular}
+ \medskip
- These global ML variables control the detail of information that is
- displayed for types, terms, theorems, goals etc.
-
- In interactive sessions, the user interface usually manages these
- global parameters of the Isabelle process, even with some concept of
- persistence. Nonetheless it is occasionally useful to manipulate ML
- variables directly, e.g.\ using @{command "ML_val"} or @{command
- "ML_command"}.
-
- Batch-mode logic sessions may be configured by putting appropriate
- ML text directly into the @{verbatim ROOT.ML} file.
+ These configuration options control the detail of information that
+ is displayed for types, terms, theorems, goals etc. See also
+ \secref{sec:config}.
\begin{description}
- \item @{ML show_types} and @{ML show_sorts} control printing of type
- constraints for term variables, and sort constraints for type
- variables. By default, neither of these are shown in output. If
- @{ML show_sorts} is set to @{ML true}, types are always shown as
- well.
+ \item @{attribute show_types} and @{attribute show_sorts} control
+ printing of type constraints for term variables, and sort
+ constraints for type variables. By default, neither of these are
+ shown in output. If @{attribute show_sorts} is enabled, types are
+ always shown as well.
Note that displaying types and sorts may explain why a polymorphic
inference rule fails to resolve with some goal, or why a rewrite
rule does not apply as expected.
- \item @{ML show_consts} controls printing of types of constants when
- displaying a goal state.
+ \item @{attribute show_consts} controls printing of types of
+ constants when displaying a goal state.
Note that the output can be enormous, because polymorphic constants
often occur at several different type instances.
- \item @{ML show_abbrevs} controls folding of constant abbreviations.
+ \item @{attribute show_abbrevs} controls folding of constant
+ abbreviations.
- \item @{ML show_brackets} controls bracketing in pretty printed
- output. If set to @{ML true}, all sub-expressions of the pretty
+ \item @{attribute show_brackets} controls bracketing in pretty
+ printed output. If enabled, all sub-expressions of the pretty
printing tree will be parenthesized, even if this produces malformed
term syntax! This crude way of showing the internal structure of
pretty printed entities may occasionally help to diagnose problems
with operator priorities, for example.
- \item @{ML Name_Space.long_names}, @{ML Name_Space.short_names}, and
- @{ML Name_Space.unique_names} control the way of printing fully
+ \item @{attribute long_names}, @{attribute short_names}, and
+ @{attribute unique_names} control the way of printing fully
qualified internal names in external form. See also
\secref{sec:antiq} for the document antiquotation options of the
same names.
- \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
- terms.
+ \item @{attribute eta_contract} controls @{text "\<eta>"}-contracted
+ printing of terms.
The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
provided @{text x} is not free in @{text f}. It asserts
@@ -167,7 +161,7 @@
F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
"\<lambda>h. F (\<lambda>x. h x)"}.
- Setting @{ML eta_contract} makes Isabelle perform @{text
+ Enabling @{attribute eta_contract} makes Isabelle perform @{text
\<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
appears simply as @{text F}.
@@ -176,33 +170,34 @@
rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
might look at terms more discretely.
- \item @{ML Goal_Display.goals_limit} controls the maximum number of
+ \item @{attribute goals_limit} controls the maximum number of
subgoals to be shown in goal output.
- \item @{ML Goal_Display.show_main_goal} controls whether the main
- result to be proven should be displayed. This information might be
+ \item @{attribute show_main_goal} controls whether the main result
+ to be proven should be displayed. This information might be
relevant for schematic goals, to inspect the current claim that has
been synthesized so far.
- \item @{ML show_hyps} controls printing of implicit hypotheses of
- local facts. Normally, only those hypotheses are displayed that are
- \emph{not} covered by the assumptions of the current context: this
- situation indicates a fault in some tool being used.
+ \item @{attribute show_hyps} controls printing of implicit
+ hypotheses of local facts. Normally, only those hypotheses are
+ displayed that are \emph{not} covered by the assumptions of the
+ current context: this situation indicates a fault in some tool being
+ used.
- By setting @{ML show_hyps} to @{ML true}, output of \emph{all}
- hypotheses can be enforced, which is occasionally useful for
- diagnostic purposes.
+ By enabling @{attribute show_hyps}, output of \emph{all} hypotheses
+ can be enforced, which is occasionally useful for diagnostic
+ purposes.
- \item @{ML show_tags} controls printing of extra annotations within
- theorems, such as internal position information, or the case names
- being attached by the attribute @{attribute case_names}.
+ \item @{attribute show_tags} controls printing of extra annotations
+ within theorems, such as internal position information, or the case
+ names being attached by the attribute @{attribute case_names}.
Note that the @{attribute tagged} and @{attribute untagged}
attributes provide low-level access to the collection of tags
associated with a theorem.
- \item @{ML show_question_marks} controls printing of question marks
- for schematic variables, such as @{text ?x}. Only the leading
+ \item @{attribute show_question_marks} controls printing of question
+ marks for schematic variables, such as @{text ?x}. Only the leading
question mark is affected, the remaining text is unchanged
(including proper markup for schematic variables that might be
relevant for user interfaces).
--- a/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 15:37:17 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue May 03 16:00:29 2011 +0200
@@ -22,7 +22,7 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Configuration options%
+\isamarkupsection{Configuration options \label{sec:config}%
}
\isamarkuptrue%
%
@@ -34,9 +34,35 @@
are easily avoided. The user may change the value of a
configuration option by means of an associated attribute of the same
name. This form of context declaration works particularly well with
- commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
-
- For historical reasons, some tools cannot take the full proof
+ commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} like
+ this:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ {\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
+\isanewline
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{note}\isamarkupfalse%
+\ {\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}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+For historical reasons, some tools cannot take the full proof
context into account and merely refer to the background theory.
This is accommodated by configuration options being declared as
``global'', which may not be changed within a local context.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 15:37:17 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 16:00:29 2011 +0200
@@ -169,76 +169,71 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
- \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\
- \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
- \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
- \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\
- \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
- \end{mldecls}
+\begin{tabular}{rcll}
+ \indexdef{}{attribute}{show\_types}\hypertarget{attribute.show-types}{\hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{show\_sorts}\hypertarget{attribute.show-sorts}{\hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
+ \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\
+ \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
+ \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}}} \\
+ \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} \\
+ \indexdef{}{attribute}{show\_hyps}\hypertarget{attribute.show-hyps}{\hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}} & : & \isa{attribute} & default \isa{false} \\
+ \indexdef{}{attribute}{show\_tags}\hypertarget{attribute.show-tags}{\hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}}} & : & \isa{attribute} & default \isa{false} \\
+ \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} \\
+ \end{tabular}
+ \medskip
- These global ML variables control the detail of information that is
- displayed for types, terms, theorems, goals etc.
-
- In interactive sessions, the user interface usually manages these
- global parameters of the Isabelle process, even with some concept of
- persistence. Nonetheless it is occasionally useful to manipulate ML
- 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}}}}.
-
- Batch-mode logic sessions may be configured by putting appropriate
- ML text directly into the \verb|ROOT.ML| file.
+ These configuration options control the detail of information that
+ is displayed for types, terms, theorems, goals etc. See also
+ \secref{sec:config}.
\begin{description}
- \item \verb|show_types| and \verb|show_sorts| control printing of type
- constraints for term variables, and sort constraints for type
- variables. By default, neither of these are shown in output. If
- \verb|show_sorts| is set to \verb|true|, types are always shown as
- well.
+ \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
+ printing of type constraints for term variables, and sort
+ constraints for type variables. By default, neither of these are
+ shown in output. If \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} is enabled, types are
+ always shown as well.
Note that displaying types and sorts may explain why a polymorphic
inference rule fails to resolve with some goal, or why a rewrite
rule does not apply as expected.
- \item \verb|show_consts| controls printing of types of constants when
- displaying a goal state.
+ \item \hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}} controls printing of types of
+ constants when displaying a goal state.
Note that the output can be enormous, because polymorphic constants
often occur at several different type instances.
- \item \verb|show_abbrevs| controls folding of constant abbreviations.
+ \item \hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}} controls folding of constant
+ abbreviations.
- \item \verb|show_brackets| controls bracketing in pretty printed
- output. If set to \verb|true|, all sub-expressions of the pretty
+ \item \hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}} controls bracketing in pretty
+ printed output. If enabled, all sub-expressions of the pretty
printing tree will be parenthesized, even if this produces malformed
term syntax! This crude way of showing the internal structure of
pretty printed entities may occasionally help to diagnose problems
with operator priorities, for example.
- \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and
- \verb|Name_Space.unique_names| control the way of printing fully
+ \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and
+ \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully
qualified internal names in external form. See also
\secref{sec:antiq} for the document antiquotation options of the
same names.
- \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of
- terms.
+ \item \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted
+ printing of terms.
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}}},
provided \isa{x} is not free in \isa{f}. It asserts
\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
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}}}.
- 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}}}
+ 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}}}
appears simply as \isa{F}.
Note that the distinction between a term and its \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded
@@ -246,33 +241,34 @@
rewriting operate modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-conversion, some other tools
might look at terms more discretely.
- \item \verb|Goal_Display.goals_limit| controls the maximum number of
+ \item \hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}} controls the maximum number of
subgoals to be shown in goal output.
- \item \verb|Goal_Display.show_main_goal| controls whether the main
- result to be proven should be displayed. This information might be
+ \item \hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}} controls whether the main result
+ to be proven should be displayed. This information might be
relevant for schematic goals, to inspect the current claim that has
been synthesized so far.
- \item \verb|show_hyps| controls printing of implicit hypotheses of
- local facts. Normally, only those hypotheses are displayed that are
- \emph{not} covered by the assumptions of the current context: this
- situation indicates a fault in some tool being used.
+ \item \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}} controls printing of implicit
+ hypotheses of local facts. Normally, only those hypotheses are
+ displayed that are \emph{not} covered by the assumptions of the
+ current context: this situation indicates a fault in some tool being
+ used.
- By setting \verb|show_hyps| to \verb|true|, output of \emph{all}
- hypotheses can be enforced, which is occasionally useful for
- diagnostic purposes.
+ By enabling \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}, output of \emph{all} hypotheses
+ can be enforced, which is occasionally useful for diagnostic
+ purposes.
- \item \verb|show_tags| controls printing of extra annotations within
- theorems, such as internal position information, or the case names
- being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}.
+ \item \hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}} controls printing of extra annotations
+ within theorems, such as internal position information, or the case
+ names being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}.
Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}
attributes provide low-level access to the collection of tags
associated with a theorem.
- \item \verb|show_question_marks| controls printing of question marks
- for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}. Only the leading
+ \item \hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}} controls printing of question
+ marks for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}. Only the leading
question mark is affected, the remaining text is unchanged
(including proper markup for schematic variables that might be
relevant for user interfaces).