--- a/src/Doc/Isar_Ref/Proof_Script.thy Wed Oct 14 15:06:42 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Wed Oct 14 15:10:32 2015 +0200
@@ -43,11 +43,11 @@
\begin{description}
- \item @{command "supply"} supports fact definitions during goal
+ \<^descr> @{command "supply"} supports fact definitions during goal
refinement: it is similar to @{command "note"}, but it operates in
backwards mode and does not have any impact on chained facts.
- \item @{command "apply"}~@{text m} applies proof method @{text m} in
+ \<^descr> @{command "apply"}~@{text m} applies proof method @{text m} in
initial position, but unlike @{command "proof"} it retains ``@{text
"proof(prove)"}'' mode. Thus consecutive method applications may be
given just as in tactic scripts.
@@ -57,7 +57,7 @@
further @{command "apply"} command would always work in a purely
backward manner.
- \item @{command "apply_end"}~@{text "m"} applies proof method @{text
+ \<^descr> @{command "apply_end"}~@{text "m"} applies proof method @{text
m} as if in terminal position. Basically, this simulates a
multi-step tactic script for @{command "qed"}, but may be given
anywhere within the proof body.
@@ -67,18 +67,18 @@
"qed"}). Thus the proof method may not refer to any assumptions
introduced in the current body, for example.
- \item @{command "done"} completes a proof script, provided that the
+ \<^descr> @{command "done"} completes a proof script, provided that the
current goal state is solved completely. Note that actual
structured proof commands (e.g.\ ``@{command "."}'' or @{command
"sorry"}) may be used to conclude proof scripts as well.
- \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
+ \<^descr> @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
shuffle the list of pending goals: @{command "defer"} puts off
sub-goal @{text n} to the end of the list (@{text "n = 1"} by
default), while @{command "prefer"} brings sub-goal @{text n} to the
front.
- \item @{command "back"} does back-tracking over the result sequence
+ \<^descr> @{command "back"} does back-tracking over the result sequence
of the latest proof command. Any proof command may return multiple
results, and this command explores the possibilities step-by-step.
It is mainly useful for experimentation and interactive exploration,
@@ -105,7 +105,7 @@
\begin{description}
- \item @{command "subgoal"} allows to impose some structure on backward
+ \<^descr> @{command "subgoal"} allows to impose some structure on backward
refinements, to avoid proof scripts degenerating into long of @{command
apply} sequences.
@@ -247,7 +247,7 @@
\begin{description}
- \item @{method rule_tac} etc. do resolution of rules with explicit
+ \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
instantiation. This works the same way as the ML tactics @{ML
Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
@@ -255,40 +255,40 @@
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
@{cite "isabelle-implementation"}).
- \item @{method cut_tac} inserts facts into the proof state as
+ \<^descr> @{method cut_tac} inserts facts into the proof state as
assumption of a subgoal; instantiations may be given as well. Note
that the scope of schematic variables is spread over the main goal
statement and rule premises are turned into new subgoals. This is
in contrast to the regular method @{method insert} which inserts
closed rule statements.
- \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
+ \<^descr> @{method thin_tac}~@{text \<phi>} deletes the specified premise
from a subgoal. Note that @{text \<phi>} may contain schematic
variables, to abbreviate the intended proposition; the first
matching subgoal premise will be deleted. Removing useless premises
from a subgoal increases its readability and can make search tactics
run faster.
- \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
+ \<^descr> @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
as new subgoals (in the original context).
- \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
+ \<^descr> @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
\emph{suffix} of variables.
- \item @{method rotate_tac}~@{text n} rotates the premises of a
+ \<^descr> @{method rotate_tac}~@{text n} rotates the premises of a
subgoal by @{text n} positions: from right to left if @{text n} is
positive, and from left to right if @{text n} is negative; the
default value is 1.
- \item @{method tactic}~@{text "text"} produces a proof method from
+ \<^descr> @{method tactic}~@{text "text"} produces a proof method from
any ML text of type @{ML_type tactic}. Apart from the usual ML
environment and the current proof context, the ML code may refer to
the locally bound values @{ML_text facts}, which indicates any
current facts used for forward-chaining.
- \item @{method raw_tactic} is similar to @{method tactic}, but
+ \<^descr> @{method raw_tactic} is similar to @{method tactic}, but
presents the goal state in its raw internal form, where simultaneous
subgoals appear as conjunction of the logical framework instead of
the usual split into several subgoals. While feature this is useful