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.

• Predeclared Operators
• Basic Semantics of Rule Infixes
• Execution Order of the Tactic Language
• Semantics of Alternative Rule Infixes
• Semantics of Other Special Operators
• Theorems with Parameters
• Functional Programming in the Tactic Language
• The Special Theorems RAISE and VALUE
• The Special Theorems EVAL and BIND
• Arithmetic Operators
• The Special Theorems INPUT and OUTPUT
• The Special Theorem ORDERED
• The Hypothesis Facility