--- a/src/Doc/Isar_Ref/Proof.thy Wed Oct 14 15:06:42 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Oct 14 15:10:32 2015 +0200
@@ -13,16 +13,16 @@
\begin{description}
- \item @{text "proof(prove)"} means that a new goal has just been
+ \<^descr> @{text "proof(prove)"} means that a new goal has just been
stated that is now to be \emph{proven}; the next command may refine
it by some proof method, and enter a sub-proof to establish the
actual result.
- \item @{text "proof(state)"} is like a nested theory mode: the
+ \<^descr> @{text "proof(state)"} is like a nested theory mode: the
context may be augmented by \emph{stating} additional assumptions,
intermediate results etc.
- \item @{text "proof(chain)"} is intermediate between @{text
+ \<^descr> @{text "proof(chain)"} is intermediate between @{text
"proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\ the
contents of the special @{fact_ref this} register) have been just picked
up in order to be used when refining the goal claimed next.
@@ -60,7 +60,7 @@
\begin{description}
- \item @{command "notepad"}~@{keyword "begin"} opens a proof state without
+ \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without
any goal statement. This allows to experiment with Isar, without producing
any persistent result. The notepad is closed by @{command "end"}.
@@ -93,10 +93,10 @@
\begin{description}
- \item @{command "next"} switches to a fresh block within a
+ \<^descr> @{command "next"} switches to a fresh block within a
sub-proof, resetting the local context to the initial one.
- \item @{command "{"} and @{command "}"} explicitly open and close
+ \<^descr> @{command "{"} and @{command "}"} explicitly open and close
blocks. Any current facts pass through ``@{command "{"}''
unchanged, while ``@{command "}"}'' causes any result to be
\emph{exported} into the enclosing context. Thus fixed variables
@@ -192,10 +192,10 @@
\begin{description}
- \item @{command "fix"}~@{text x} introduces a local variable @{text
+ \<^descr> @{command "fix"}~@{text x} introduces a local variable @{text
x} that is \emph{arbitrary, but fixed.}
- \item @{command "assume"}~@{text "a: \<phi>"} and @{command
+ \<^descr> @{command "assume"}~@{text "a: \<phi>"} and @{command
"presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
assumption. Subsequent results applied to an enclosing goal (e.g.\
by @{command_ref "show"}) are handled as follows: @{command
@@ -206,7 +206,7 @@
@{keyword_ref "and"}; the resulting list of current facts consists
of all of these concatenated.
- \item @{command "def"}~@{text "x \<equiv> t"} introduces a local
+ \<^descr> @{command "def"}~@{text "x \<equiv> t"} introduces a local
(non-polymorphic) definition. In results exported from the context,
@{text x} is replaced by @{text t}. Basically, ``@{command
"def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
@@ -264,11 +264,11 @@
\begin{description}
- \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
+ \<^descr> @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous
higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
- \item @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but
+ \<^descr> @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but
matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement. Also
note that @{keyword "is"} is not a separate command, but part of
others (such as @{command "assume"}, @{command "have"} etc.).
@@ -320,12 +320,12 @@
\begin{description}
- \item @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
+ \<^descr> @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
@{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. Note that
attributes may be involved as well, both on the left and right hand
sides.
- \item @{command "then"} indicates forward chaining by the current
+ \<^descr> @{command "then"} indicates forward chaining by the current
facts in order to establish the goal to be claimed next. The
initial proof method invoked to refine that will be offered the
facts to do ``anything appropriate'' (see also
@@ -335,19 +335,19 @@
facts into the goal state before operation. This provides a simple
scheme to control relevance of facts in automated proof search.
- \item @{command "from"}~@{text b} abbreviates ``@{command
+ \<^descr> @{command "from"}~@{text b} abbreviates ``@{command
"note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
equivalent to ``@{command "from"}~@{text this}''.
- \item @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command
+ \<^descr> @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command
"from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining
is from earlier facts together with the current ones.
- \item @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being
+ \<^descr> @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being
currently indicated for use by a subsequent refinement step (such as
@{command_ref "apply"} or @{command_ref "proof"}).
- \item @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally
+ \<^descr> @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally
similar to @{command "using"}, but unfolds definitional equations
@{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.
@@ -445,7 +445,7 @@
\begin{description}
- \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
+ \<^descr> @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
@{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
\<phi>"} to be put back into the target context. An additional @{syntax
context} specification may build up an initial proof context for the
@@ -453,11 +453,11 @@
well, see also @{syntax "includes"} in \secref{sec:bundle} and
@{syntax context_elem} in \secref{sec:locale}.
- \item @{command "theorem"}, @{command "corollary"}, and @{command
+ \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command
"proposition"} are the same as @{command "lemma"}. The different command
names merely serve as a formal comment in the theory source.
- \item @{command "schematic_goal"} is similar to @{command "theorem"},
+ \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"},
but allows the statement to contain unbound schematic variables.
Under normal circumstances, an Isar proof text needs to specify
@@ -467,14 +467,14 @@
proofs is lost, which also impacts performance, because proof
checking is forced into sequential mode.
- \item @{command "have"}~@{text "a: \<phi>"} claims a local goal,
+ \<^descr> @{command "have"}~@{text "a: \<phi>"} claims a local goal,
eventually resulting in a fact within the current logical context.
This operation is completely independent of any pending sub-goals of
an enclosing goal statements, so @{command "have"} may be freely
used for experimental exploration of potential results within a
proof body.
- \item @{command "show"}~@{text "a: \<phi>"} is like @{command
+ \<^descr> @{command "show"}~@{text "a: \<phi>"} is like @{command
"have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
sub-goal for each one of the finished result, after having been
exported into the corresponding context (at the head of the
@@ -487,16 +487,16 @@
following message:
@{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
- \item @{command "hence"} abbreviates ``@{command "then"}~@{command
+ \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command
"have"}'', i.e.\ claims a local goal to be proven by forward
chaining the current facts. Note that @{command "hence"} is also
equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
- \item @{command "thus"} abbreviates ``@{command "then"}~@{command
+ \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command
"show"}''. Note that @{command "thus"} is also equivalent to
``@{command "from"}~@{text this}~@{command "show"}''.
- \item @{command "print_statement"}~@{text a} prints facts from the
+ \<^descr> @{command "print_statement"}~@{text a} prints facts from the
current theory or proof context in long statement form, according to
the syntax for @{command "lemma"} given above.
@@ -576,7 +576,7 @@
\begin{description}
- \item @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary
+ \<^descr> @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary
@{fact calculation} register as follows. The first occurrence of
@{command "also"} in some calculational thread initializes @{fact
calculation} by @{fact this}. Any subsequent @{command "also"} on
@@ -586,7 +586,7 @@
current context, unless alternative rules are given as explicit
arguments.
- \item @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact
+ \<^descr> @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact
calculation} in the same way as @{command "also"}, and concludes the
current calculational thread. The final result is exhibited as fact
for forward chaining towards the next goal. Basically, @{command
@@ -596,22 +596,22 @@
"show"}~@{text ?thesis}~@{command "."}'' and ``@{command
"finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
- \item @{command "moreover"} and @{command "ultimately"} are
+ \<^descr> @{command "moreover"} and @{command "ultimately"} are
analogous to @{command "also"} and @{command "finally"}, but collect
results only, without applying rules.
- \item @{command "print_trans_rules"} prints the list of transitivity
+ \<^descr> @{command "print_trans_rules"} prints the list of transitivity
rules (for calculational commands @{command "also"} and @{command
"finally"}) and symmetry rules (for the @{attribute symmetric}
operation and single step elimination patters) of the current
context.
- \item @{attribute trans} declares theorems as transitivity rules.
+ \<^descr> @{attribute trans} declares theorems as transitivity rules.
- \item @{attribute sym} declares symmetry rules, as well as
+ \<^descr> @{attribute sym} declares symmetry rules, as well as
@{attribute "Pure.elim"}@{text "?"} rules.
- \item @{attribute symmetric} resolves a theorem with some rule
+ \<^descr> @{attribute symmetric} resolves a theorem with some rule
declared as @{attribute sym} in the current context. For example,
``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
swapped fact derived from that assumption.
@@ -751,11 +751,11 @@
\begin{description}
- \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof
+ \<^descr> @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof
method @{text "m\<^sub>1"}; facts for forward chaining are passed if so
indicated by @{text "proof(chain)"} mode.
- \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by
+ \<^descr> @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by
proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.
If the goal had been @{text "show"} (or @{text "thus"}), some
pending sub-goal is solved as well by the rule resulting from the
@@ -768,7 +768,7 @@
@{command "have"}, or weakening the local context by replacing
occurrences of @{command "assume"} by @{command "presume"}.
- \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal
+ \<^descr> @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal
proof}\index{proof!terminal}; it abbreviates @{command
"proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with
backtracking across both methods. Debugging an unsuccessful
@@ -777,15 +777,15 @@
@{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
problem.
- \item ``@{command ".."}'' is a \emph{standard
+ \<^descr> ``@{command ".."}'' is a \emph{standard
proof}\index{proof!standard}; it abbreviates @{command "by"}~@{text
"standard"}.
- \item ``@{command "."}'' is a \emph{trivial
+ \<^descr> ``@{command "."}'' is a \emph{trivial
proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
"this"}.
- \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
+ \<^descr> @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
pretending to solve the pending claim without further ado. This
only works in interactive development, or if the @{attribute
quick_and_dirty} is enabled. Facts emerging from fake
@@ -796,7 +796,7 @@
The most important application of @{command "sorry"} is to support
experimentation and top-down proof development.
- \item @{method standard} refers to the default refinement step of some
+ \<^descr> @{method standard} refers to the default refinement step of some
Isar language elements (notably @{command proof} and ``@{command ".."}'').
It is \emph{dynamically scoped}, so the behaviour depends on the
application environment.
@@ -862,7 +862,7 @@
\begin{description}
- \item @{command "print_rules"} prints rules declared via attributes
+ \<^descr> @{command "print_rules"} prints rules declared via attributes
@{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
(Pure) dest} of Isabelle/Pure.
@@ -870,7 +870,7 @@
rule declarations of the classical reasoner
(\secref{sec:classical}).
- \item ``@{method "-"}'' (minus) inserts the forward chaining facts as
+ \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as
premises into the goal, and nothing else.
Note that command @{command_ref "proof"} without any method actually
@@ -878,7 +878,7 @@
method; thus a plain \emph{do-nothing} proof step would be ``@{command
"proof"}~@{text "-"}'' rather than @{command "proof"} alone.
- \item @{method "goal_cases"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
+ \<^descr> @{method "goal_cases"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
into cases within the context (see also \secref{sec:cases-induct}). The
specified case names are used if present; otherwise cases are numbered
starting from 1.
@@ -888,7 +888,7 @@
premises, and @{command let} variable @{variable_ref ?case} refer to the
conclusion.
- \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
+ \<^descr> @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
@{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
modulo unification of schematic type and term variables. The rule
structure is not taken into account, i.e.\ meta-level implication is
@@ -899,7 +899,7 @@
@{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the
proof context.
- \item @{method assumption} solves some goal by a single assumption
+ \<^descr> @{method assumption} solves some goal by a single assumption
step. All given facts are guaranteed to participate in the
refinement; this means there may be only 0 or 1 in the first place.
Recall that @{command "qed"} (\secref{sec:proof-steps}) already
@@ -907,11 +907,11 @@
proofs usually need not quote the @{method assumption} method at
all.
- \item @{method this} applies all of the current facts directly as
+ \<^descr> @{method this} applies all of the current facts directly as
rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
"by"}~@{text this}''.
- \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
+ \<^descr> @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
argument in backward manner; facts are used to reduce the rule
before applying it to the goal. Thus @{method (Pure) rule} without facts
is plain introduction, while with facts it becomes elimination.
@@ -923,7 +923,7 @@
behaviour of @{command "proof"} and ``@{command ".."}'' (double-dot) steps
(see \secref{sec:proof-steps}).
- \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
+ \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
@{attribute (Pure) dest} declare introduction, elimination, and
destruct rules, to be used with method @{method (Pure) rule}, and similar
tools. Note that the latter will ignore rules declared with
@@ -934,10 +934,10 @@
present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
"Pure.intro"}.
- \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
+ \<^descr> @{attribute (Pure) rule}~@{text del} undeclares introduction,
elimination, or destruct rules.
- \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
+ \<^descr> @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} in canonical right-to-left
order, which means that premises stemming from the @{text "a\<^sub>i"}
emerge in parallel in the result, without interfering with each
@@ -949,7 +949,7 @@
(underscore), which refers to the propositional identity rule in the
Pure theory.
- \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
+ \<^descr> @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
instantiation of term variables. The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
substituted for any schematic variables occurring in a theorem from
left to right; ``@{text _}'' (underscore) indicates to skip a
@@ -960,7 +960,7 @@
be specified: the instantiated theorem is exported, and these
variables become schematic (usually with some shifting of indices).
- \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
+ \<^descr> @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
performs named instantiation of schematic type and term variables
occurring in a theorem. Schematic variables have to be specified on
the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may
@@ -988,7 +988,7 @@
\begin{description}
- \item @{command "method_setup"}~@{text "name = text description"}
+ \<^descr> @{command "method_setup"}~@{text "name = text description"}
defines a proof method in the current context. The given @{text
"text"} has to be an ML expression of type
@{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
@@ -1096,7 +1096,7 @@
\begin{description}
- \item @{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
+ \<^descr> @{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
appropriate proof method (such as @{method_ref cases} and @{method_ref
induct}). The command ``@{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"}''
@@ -1109,17 +1109,17 @@
re-use @{text c}. So @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} is the same
as @{command "case"}~@{text "c: (c x\<^sub>1 \<dots> x\<^sub>m)"}.
- \item @{command "print_cases"} prints all local contexts of the
+ \<^descr> @{command "print_cases"} prints all local contexts of the
current state, using Isar proof language notation.
- \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
+ \<^descr> @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
refers to the \emph{prefix} of the list of premises. Each of the
cases @{text "c\<^sub>i"} can be of the form @{text "c[h\<^sub>1 \<dots> h\<^sub>n]"} where
the @{text "h\<^sub>1 \<dots> h\<^sub>n"} are the names of the hypotheses in case @{text "c\<^sub>i"}
from left to right.
- \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
+ \<^descr> @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
names for the conclusions of a named premise @{text c}; here @{text
"d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula
built by nesting a binary connective (e.g.\ @{text "\<or>"}).
@@ -1129,7 +1129,7 @@
whole. The need to name subformulas only arises with cases that
split into several sub-cases, as in common co-induction rules.
- \item @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames
+ \<^descr> @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames
the innermost parameters of premises @{text "1, \<dots>, n"} of some
theorem. An empty list of names may be given to skip positions,
leaving the present parameters unchanged.
@@ -1137,7 +1137,7 @@
Note that the default usage of case rules does \emph{not} directly
expose parameters to the proof context.
- \item @{attribute consumes}~@{text n} declares the number of ``major
+ \<^descr> @{attribute consumes}~@{text n} declares the number of ``major
premises'' of a rule, i.e.\ the number of facts to be consumed when
it is applied by an appropriate proof method. The default value of
@{attribute consumes} is @{text "n = 1"}, which is appropriate for
@@ -1216,7 +1216,7 @@
\begin{description}
- \item @{method cases}~@{text "insts R"} applies method @{method
+ \<^descr> @{method cases}~@{text "insts R"} applies method @{method
rule} with an appropriate case distinction theorem, instantiated to
the subjects @{text insts}. Symbolic case names are bound according
to the rule's local contexts.
@@ -1243,7 +1243,7 @@
"(no_simp)"} option can be used to disable pre-simplification of
cases (see the description of @{method induct} below for details).
- \item @{method induct}~@{text "insts R"} and
+ \<^descr> @{method induct}~@{text "insts R"} and
@{method induction}~@{text "insts R"} are analogous to the
@{method cases} method, but refer to induction rules, which are
determined as follows:
@@ -1300,7 +1300,7 @@
pending variables in the rule. Such schematic induction rules
rarely occur in practice, though.
- \item @{method coinduct}~@{text "inst R"} is analogous to the
+ \<^descr> @{method coinduct}~@{text "inst R"} is analogous to the
@{method induct} method, but refers to coinduction rules, which are
determined as follows:
@@ -1406,10 +1406,10 @@
\begin{description}
- \item @{command "print_induct_rules"} prints cases and induct rules
+ \<^descr> @{command "print_induct_rules"} prints cases and induct rules
for predicates (or sets) and types of the current context.
- \item @{attribute cases}, @{attribute induct}, and @{attribute
+ \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute
coinduct} (as attributes) declare rules for reasoning about
(co)inductive predicates (or sets) and types, using the
corresponding methods of the same name. Certain definitional
@@ -1472,7 +1472,7 @@
\begin{description}
- \item @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
+ \<^descr> @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
| (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} states a rule for case
splitting into separate subgoals, such that each case involves new
parameters and premises. After the proof is finished, the resulting rule
@@ -1502,7 +1502,7 @@
statements, as well as @{command print_statement} to print existing rules
in a similar format.
- \item @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"}
+ \<^descr> @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"}
states a generalized elimination rule with exactly one case. After the
proof is finished, it is activated for the subsequent proof text: the
context is augmented via @{command fix}~@{text "\<^vec>x"} @{command
@@ -1529,7 +1529,7 @@
\quad @{command "fix"}~@{text "\<^vec>x"}~@{command "assume"}@{text "\<^sup>* a: \<^vec>A \<^vec>x"} \\
\end{matharray}
- \item @{command guess} is similar to @{command obtain}, but it derives the
+ \<^descr> @{command guess} is similar to @{command obtain}, but it derives the
obtained context elements from the course of tactical reasoning in the
proof. Thus it can considerably obscure the proof: it is classified as
\emph{improper}.