ETR-AUTO-SUGGEST : MEXPR

ETR-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
nat-etree.

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:

 <n>ETR-AUTO-SUGGEST 

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage