334 instantiate variables, it cannot make other subgoals unprovable. |
334 instantiate variables, it cannot make other subgoals unprovable. |
335 |
335 |
336 \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML |
336 \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML |
337 bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac}, |
337 bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac}, |
338 @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do |
338 @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do |
339 not instantiate schematic variables in the goal state. |
339 not instantiate schematic variables in the goal state.% |
|
340 \footnote{Strictly speaking, matching means to treat the unknowns in the goal |
|
341 state as constants, but these tactics merely discard unifiers that would |
|
342 update the goal state. In rare situations (where the conclusion and |
|
343 goal state have flexible terms at the same position), the tactic |
|
344 will fail even though an acceptable unifier exists.} |
|
345 These tactics were written for a specific application within the classical reasoner. |
340 |
346 |
341 Flexible subgoals are not updated at will, but are left alone. |
347 Flexible subgoals are not updated at will, but are left alone. |
342 Strictly speaking, matching means to treat the unknowns in the goal |
|
343 state as constants; these tactics merely discard unifiers that would |
|
344 update the goal state. |
|
345 |
|
346 \end{description} |
348 \end{description} |
347 *} |
349 *} |
348 |
350 |
349 |
351 |
350 subsection {* Explicit instantiation within a subgoal context *} |
352 subsection {* Explicit instantiation within a subgoal context *} |