Home /
Examples
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
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