**assign:**- The
**assign**command takes two string arguments, both terms. If the second term matches the first, the induced substitution is applied to both sides of the equation under construction. **assignit:**- The
**assignit**command takes one string argument. It has the effect of the**assign**command with its argument as first argument and the currently selected subterm as second argument. **assigninto:**- The
**assigninto**command takes two arguments, a free variable and a term. Each side of the equation under construction is replaced by the result of substituting the appropriate side of the equation for the variable argument in the term argument. **unification:**- The
**unification**command takes one string argument. It applies substitutions into both the argument (interpreted as a term) and both sides of the current equation, in such a way as to make the new form of the argument the same as the new form of the currently selected subterm, if this is possible. If it is not possible, an error message is issued and nothing in the environment is changed. Restriction: terms with free occurrences of bound variables will not be matched with free variables, since this makes it hard to determine whether global substitutions are legitimate.**u**is an abbreviation for this command. **ul:**- As
**unification**, except that the argument is the name of a theorem and the left side of that theorem is unified with the currently selected subterm. The effect is to attempt to make substitutions which make the theorem applicable. **ur:**- As
**unification**, except that the argument is the name of a theorem and the right side of that theorem is unified with the currently selected subterm. The effect is to attempt to make substitutions which make the converse of the theorem applicable. **initializecounter:**- This command takes a unit argument. It has
the effect of resetting the new variable counter to 1.
**ruleintro:**- The
**ruleintro**command takes a string argument, a term. The string argument is introduced as an embedded theorem attached to the current subterm by the`=>`infix of direct theorem application.**ri**is an abbreviation for**ruleintro**. **revruleintro:**- The
**revruleintro**command takes a string argument, a term. The string argument is introduced as an embedded theorem attached to the current subterm by the`<=`infix of converse theorem application.**rri**is an abbreviation for**revruleintro**. **inputri:**- The
**inputri**command takes a string argument. It is used to supply theorems to be applied to the`INPUT`tactic. When paused after an execution of`INPUT`, issue the**inputri**command with the desired argument, then issue`;`to resume execution.**iri**is an abbreviation for`inputri`. **targetruleintro:**- The
**targetruleintro**command takes a string argument, a term. It will cause a theorem to be introduced which will have the effect of rewriting the selected subterm to the argument, if there is such a theorem.**tri**is an abbreviation for**targetruleintro**. **matchtri:**- As
`targetruleintro`, but looks for theorems which will give a result matching the argument in structure, rather than an identical result. Theorems are displayed as a side-effect.`mtri`is an abbreviation for`matchtri`. **anothermatchtri:**- If issued immediately after
`matchtri`(or`anothermatchtri`this command will search for another suitable theorem. Theorems are displayed as a side-effect.`amtri`is an abbreviation for`matchtri`. **tri2:**- As
`targetruleintro`, except that it searches for two-step proofs. Very slow! **trimetric:**- Takes two arguments, an integer and a target term.
Looks for a proof that the selected subterm is equal to the target
term, in a number of steps bounded by the integer argument. Proofs
must satisfy a condition of ``approaching'' the target term at each
step; it does not search all possible proofs. Experimental!
**droprule:**- The
**droprule**command takes a unit argument. If the currently selected subterm has`=>`or`<=`as top-level infix, the indicated embedded theorem is dropped. **altruleintro:**- This command takes one string argument, a term.
If the currently selected subterm has
`=>`or`<=`as top-level infix, the argument is appended to the left subterm (the embedded theorem) using the`=>>`infix. This is different from the effect in Mark2, though the signalled intention to rewrite is the same.**ari**is an abbreviation for**altruleintro**. **altrevruleintro:**- This command takes one string argument, a term.
If the currently selected subterm has
`=>`or`<=`as top-level infix, the argument is appended to the left subterm (the embedded theorem) using the`<<=`infix. This is different from the effect in Mark2, though the signalled intention to rewrite is the same.**arri**is an abbreviation for**altruleintro**. **execute:**- This command takes a unit argument. The tactic
interpreter is invoked to carry out all intentions to rewrite
indicated by embedded theorems, following a depth-first strategy.
**ex**is an abbreviation for**execute**. **steps:**- This command takes a unit argument. This is a trace
command. The tactic interpreter is simulated, carrying out intentions
to rewrite indicated by embedded theorems which are applied to terms
containing no embedded theorems (innermost applications of embedded
theorems). One step is carried out at a time: enter
`;`to see the next step or`e;`to quit (in old versions, hit enter to see the next step or q to quit). **stepsnorules:**- This command takes a unit argument. As
`steps`, except that embedded theorems are not displayed in the terms, and new terms are displayed only when there are changes other than changes to embedded theorems. This can conceivably go into an infinite loop, which is not the case for`steps`. **settracelevel:**- This command takes a string argument followed by
an integer argument. The theorem (in intention, tactic) named by the
string argument is assigned a ``trace level'' equal to the integer
argument. When
`steps`is executed, theorems with a high enough ``trace level'' (see next command) are executed all at once instead of being traced through their execution. This allows fine-tuning of the trace function provided by`steps`. **settrace:**- This command sets the cutoff value of ``trace level''
above which the
`steps`command executes tactics completely in one step. See previous command. **applyenv:**- This command takes a single string argument, the name
of a saved environment. The saved environment represented by the
argument is applied as a rewrite rule in the direct sense to the
currently selected subterm.
**applyconvenv:**- This command takes a single string argument, the name
of a saved environment. The saved environment represented by the
argument is applied as a rewrite rule in the converse sense to the
currently selected subterm.
**cmatch:**- This command takes a unit argument. It turns
commutative matching on or off. Strict matching is still used by the
on-success and on-failure rule infixes. Not available in the official
release, but found in a posted draft version. We have decided not
to use this.