UNTRANSLATE
See
user-defined-functions-table
.
Major Section:
ACL2-BUILT-INS
