This article presents a pattern-based language designed to select (a set of) subterms of a given term in a concise and robust way. Building on this language, we implement a single-step rewriting tactic in the Isabelle theorem prover, which removes the need for obscure "occurrence numbers" for subterm selection. The language was inspired by the \emph{language of patterns} of Gonthier and Tassi, but provides an elegant way of handling bound variables and a modular semantics.

翻译：此篇文章呈现一种基于模式的语言, 旨在以简洁和稳健的方式选择特定术语的子术语( 一组) 。 我们在此语言的基础上, 在伊莎贝尔理论验证器中实施单步重写策略, 从而消除了在子术语选择中使用模糊的“ 常数 ” 的需要。 该语言受贡提尔和塔西的\ emph{ 模式语言} 的启发, 但它提供了一种优雅的处理约束变量和模块语义的方法 。