The code below is based on code published in the following paper.

Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language, by Amy Felty.Journal of Automated Reasoning, 11(1):43-81, August 1993. (Postscript), (Abstract)).

- goals.mod:
Definition of the goal data structure and some useful relations
on goals.
- inter_tacs.mod: .
Tactics to support interactive theorem proving.
- tacticals.mod: .
Some general tacticals.

Home / Examples