UNTRANS-TABLE

associates a function symbol with a macro for printing user-level terms 
Major Section:  SWITCHES-PARAMETERS-AND-MODES


Examples:
ACL2 !>(untrans-table (w state))
((BINARY-+ + . T)
 (BINARY-* * . T)
 (BINARY-APPEND APPEND . T)
 (BINARY-LOGAND LOGAND . T)
 (BINARY-LOGIOR LOGIOR . T)
 (BINARY-LOGXOR LOGXOR . T)
 (BINARY-LOGEQV LOGEQV . T)
 (BINARY-POR POR . T)
 (BINARY-PAND PAND . T))

See table for a general discussion of tables.

See add-macro-fn for a more general discussion of this table and for a way to associate a macro name with a function name in theory events.