ETR-AUTO-SUGGEST : MEXPRETR-AUTO-SUGGEST is a top-level command.
Given an eproof, suggest flag settings for
an automatic proof of the same theorem. Such an eproof may
be the result of translating a natural deduction proof using
This will show all of the instantiations (and primitive substitutions)
that are necessary for the proof, and suggest settings for
NUM-OF-DUPS, MS98-NUM-OF-DUPS, and MAX-MATES.
The command format for ETR-AUTO-SUGGEST is:
TPS documentation homepage