Tactics for Theorem Proving
The code below is based on code published in the following paper.
Implementing Tactics and Tacticals in a Higher-Order Logic
by Amy Felty.
Journal of Automated Reasoning, 11(1):43-81, August 1993.
Definition of the goal data structure and some useful relations
- inter_tacs.mod: .
Tactics to support interactive theorem proving.
- tacticals.mod: .
Some general tacticals.