next up previous contents
Next: Predeclared Operators Up: Mark2 Prover Documentation Previous: The Definition Facility

The Tactic Language

The tactic language of Mark2 is actually a predeclared part of the internal language. Tactics are represented as equations in theories, and this is achieved via a device for representing theorems and operations on theorems as objects in the internal language of each theory.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997