--- a/src/Doc/Implementation/Tactic.thy Fri Oct 16 10:11:20 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy Fri Oct 16 14:53:26 2015 +0200
@@ -70,8 +70,6 @@
@{index_ML Goal.conclude: "thm -> thm"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML "Goal.init"}~@{text C} initializes a tactical goal from
the well-formed proposition @{text C}.
@@ -86,8 +84,6 @@
\<^descr> @{ML "Goal.conclude"}~@{text "thm"} removes the goal
protection, even if there are pending subgoals.
-
- \end{description}
\<close>
@@ -150,8 +146,6 @@
The main well-formedness conditions for proper tactics are
summarized as follows.
- \begin{itemize}
-
\<^item> General tactic failure is indicated by an empty result, only
serious faults may produce an exception.
@@ -164,7 +158,6 @@
\<^item> Range errors in subgoal addressing produce an empty result.
- \end{itemize}
Some of these conditions are checked by higher-level goal
infrastructure (\secref{sec:struct-goals}); others are not checked
@@ -187,8 +180,6 @@
@{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> Type @{ML_type tactic} represents tactics. The
well-formedness conditions described above need to be observed. See
also @{file "~~/src/Pure/General/seq.ML"} for the underlying
@@ -233,8 +224,6 @@
\<^descr> @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
@{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but
without changing the main goal protection.
-
- \end{description}
\<close>
@@ -264,8 +253,6 @@
sequence enumerates all possibilities of the following choices (if
applicable):
- \begin{enumerate}
-
\<^enum> selecting one of the rules given as argument to the tactic;
\<^enum> selecting a subgoal premise to eliminate, unifying it against
@@ -274,7 +261,6 @@
\<^enum> unifying the conclusion of the subgoal to the conclusion of
the rule.
- \end{enumerate}
Recall that higher-order unification may produce multiple results
that are enumerated here.
@@ -295,8 +281,6 @@
@{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state
using the given theorems, which should normally be introduction
rules. The tactic resolves a rule's conclusion with subgoal @{text
@@ -350,7 +334,6 @@
These tactics were written for a specific application within the classical reasoner.
Flexible subgoals are not updated at will, but are left alone.
- \end{description}
\<close>
@@ -419,8 +402,6 @@
@{index_ML rename_tac: "string list -> int -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
rule @{text thm} with the instantiations @{text insts}, as described
above, and then performs resolution on subgoal @{text i}.
@@ -449,7 +430,6 @@
parameters of subgoal @{text i} according to the provided @{text
names} (which need to be distinct identifiers).
- \end{description}
For historical reasons, the above instantiation tactics take
unparsed string arguments, which makes them hard to use in general
@@ -473,8 +453,6 @@
@{index_ML flexflex_tac: "Proof.context -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal
@{text i} by @{text n} positions: from right to left if @{text n} is
positive, and from left to right if @{text n} is negative.
@@ -491,8 +469,6 @@
unification. To prevent this, use @{ML Rule_Insts.res_inst_tac} to
instantiate some variables in a rule. Normally flex-flex constraints
can be ignored; they often disappear as unknowns get instantiated.
-
- \end{description}
\<close>
@@ -513,8 +489,6 @@
@{index_ML_op COMP: "thm * thm -> thm"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
@{text "i"} using @{text "rule"}, without lifting. The @{text
"rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
@@ -534,7 +508,6 @@
\<^descr> @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose
(thm\<^sub>1, 1, thm\<^sub>2)"}.
- \end{description}
\begin{warn}
These low-level operations are stepping outside the structure
@@ -581,8 +554,6 @@
@{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential
composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal
state, it returns all states reachable in two steps by applying
@@ -621,8 +592,6 @@
"(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
The other primed tacticals work analogously.
-
- \end{description}
\<close>
@@ -641,8 +610,6 @@
@{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal
state and returns the resulting sequence, if non-empty; otherwise it
returns the original state. Thus, it applies @{text "tac"} at most
@@ -672,15 +639,11 @@
\<^descr> @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
-
- \end{description}
\<close>
text %mlex \<open>The basic tactics and tacticals considered above follow
some algebraic laws:
- \begin{itemize}
-
\<^item> @{ML all_tac} is the identity element of the tactical @{ML_op
"THEN"}.
@@ -692,8 +655,6 @@
\<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
functions over more basic combinators (ignoring some internal
implementation tricks):
-
- \end{itemize}
\<close>
ML \<open>
@@ -747,8 +708,6 @@
@{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac
n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}. It
applies the @{text tac} to all the subgoals, counting downwards.
@@ -774,8 +733,6 @@
@{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op
THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the
corresponding range of subgoals, counting downwards.
-
- \end{description}
\<close>
@@ -800,8 +757,6 @@
@{index_ML CHANGED: "tactic -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the
goal state and returns a sequence consisting of those result goal
states that are satisfactory in the sense of @{text "sat"}.
@@ -810,8 +765,6 @@
state and returns precisely those states that differ from the
original state (according to @{ML Thm.eq_thm}). Thus @{ML
CHANGED}~@{text "tac"} always has some effect on the state.
-
- \end{description}
\<close>
@@ -824,8 +777,6 @@
@{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if
@{text "sat"} returns true. Otherwise it applies @{text "tac"},
then recursively searches from each element of the resulting
@@ -839,8 +790,6 @@
\<^descr> @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to
search for states having fewer subgoals than the given state. Thus,
it insists upon solving at least one subgoal.
-
- \end{description}
\<close>
@@ -857,8 +806,6 @@
However, they do not enumerate all solutions; they terminate after
the first satisfactory result from @{text "tac"}.
- \begin{description}
-
\<^descr> @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first
search to find states for which @{text "sat"} is true. For most
applications, it is too slow.
@@ -880,8 +827,6 @@
the result of applying @{text "tac\<^sub>0"} to the goal state. This
tactical permits separate tactics for starting the search and
continuing the search.
-
- \end{description}
\<close>
@@ -895,8 +840,6 @@
@{index_ML DETERM: "tactic -> tactic"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to
the goal state if it satisfies predicate @{text "sat"}, and applies
@{text "tac\<^sub>2"}. It is a conditional tactical in that only one of
@@ -915,8 +858,6 @@
\<^descr> @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal
state and returns the head of the resulting sequence. @{ML DETERM}
limits the search space by making its argument deterministic.
-
- \end{description}
\<close>
@@ -930,8 +871,6 @@
@{index_ML size_of_thm: "thm -> int"} \\
\end{mldecls}
- \begin{description}
-
\<^descr> @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
"thm"} has fewer than @{text "n"} premises.
@@ -948,8 +887,6 @@
"thm"}, namely the number of variables, constants and abstractions
in its conclusion. It may serve as a distance function for
@{ML BEST_FIRST}.
-
- \end{description}
\<close>
end