Add-fgl-rewrites
Enable some rewrite rules for use in FGL
Adds the given rewrite rule runes to the fgl-rewrite-rules table so
that each such rule will be attempted when terms with its LHS's leading
function symbol is encountered. The exact form of the rule that is used
depends on the invocation: if a name given is simply a symbol, then the formula
of that theorem or function name is used. If a name is instead a :rewrite
or :definition rune, then the corresponding lemma is used. A
:formula rune (which is not a valid ACL2 rune but is a valid FGL rune) is
treated the same as a bare symbol.
Subtopics
- Add-fgl-rewrite
- Alias for add-fgl-rewrites that just takes one name.
