next up previous contents
Next: Basic Control Structures Up: Logical and Programming Style Previous: The Logical Preamble

Programming Style

The development of the tactic language has largely been driven by the requirements of the ABSTRACT and (to a lesser extent) REDUCE tactics. An outline of the development of some simple example programs culminating in the development of limited (predicative) abstraction and reduction tactics and an introduction to some of their applications seems natural as an introduction to programming in the tactic language. These tactics are no longer used in practice, with the introduction of variable binding and the BIND and EVAL built-in tactics, but tactic programming remains useful.

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