src/Doc/Isar_Ref/Proof_Script.thy

     @@{command prefer} @{syntax nat}
   \<close>}
 
   \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.
 
   Facts are passed to @{text m} as indicated by the goal's
   forward-chain mode, and are \emph{consumed} afterwards.  Thus any
   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.
 
   No facts are passed to @{text m} here.  Furthermore, the static
   context is that of the enclosing goal (as for actual @{command
   "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,
   and should be avoided in finished proofs.
 

     params: @'for' '\<dots>'? (('_' | @{syntax name})+)
   \<close>}
 
   \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.
 
   The current goal state, which is essentially a hidden part of the Isar/VM
   configurtation, is turned into a proof context and remaining conclusion.

     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   \<close>}
 
 \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"}).
 
   Multiple rules may be only given if there is no instantiation; then
   @{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
   for debugging of complex method definitions, it should not never
   appear in production theories.