Utilities used in ACL2s.
This is a collection of utilities used in ACL2s, the ACL2 Sedan.
- A macro that
creates an arbitrary-arity macro given a binary function
and associates the function name with the macro name using
- The well-founded less-than relation on natural numbers.
- The ACL2s version of skip-proofs.
- A proof-builder command that repeats the given instructions
until all goals have been proved
- A version of thm with testing disabled.
- A version of defthm with testing disabled.