MetaPRL Tactic Layer

The proof mechanism used in MetaPRL is LCF-style tactic proving. The tactic layer defines functions (called tacticals) to combine tactics, and it also defines term rewriting and conversionals. There are several modules in the tactic layer, including: