A Tactic Calculus - Full version
Andrew Martin, P. H. B. Gardiner, Jim Woodcock · ePrints Soton (University of Southampton) · 1996
We present a very general language for expressing tactic programs. The paper describes some essential tactic combinators (tacticals), and gives them a formal semantics. Those definitions are used to produce a complete calculus for reasoning about tactics written in this language. The language is extended to cover structural combinators which enable the tactics to be precisely targeted upon particular sub-expressions.