Documentation

Tactics

The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.