next up previous contents
Next: Semantics of Alternative Rule Up: The Tactic Language Previous: Basic Semantics of Rule

Execution Order of the Tactic Language

When the execute command is issued, all embedded theorems in the selected subterm of the right side of the current equation are applied as rewrite rules. The rule is that innermost embedded theorems are applied first; this includes embedded theorems introduced by the execution of the tactic interpreter! It means that rewrite rules are always applied to terms which themselves contain no embedded theorems.

This is only a preliminary picture of the execution order; but it is needed to explain what is going on below.

The debugger steps carries out this process one step at a time, with some parallelism: it applies all and only innermost embedded theorems.

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