Next: Miscellaneous Functions
Up: Appendix A: Summary
Previous: Term Destructors
- set_auto_tactic: tok
void.
-
Set auto--tactic to be the ML expression represented by the token.
- show_auto_tactic: void
tok.
-
Displays the current setting of the auto--tactic.
Richard Eaton
Thu Sep 14 08:45:18 EDT 1995