PRL Seminars

The use of tactics for interactive theorem proving is widespread. Systems based on tactics typically employ an auxiliary data structure, such as a stack or a tee, to help manage such tasks as the composition of validations and selection of subgoals.

This report describes a logic-independent implementation of a tactic trees and its X-windows interface for structure-oriented editing. The system is implemented in Standard ML of New Jersey using CML and eXene.

This is joint work with Timothy Griffin.