|
|
|---|
|
|
|
|---|
Notion of instance of a second-order theorem.
An instance of a second-order theorem is an ACL2 theorem
introduced via defthm-inst,
which replaces function variables that the second-order theorem depends on
with functions of matching arities.
This macro specifies the replacement as an
The new theorem is second-order if it still depends on function variables,
otherwise it is first-order.
defthm-inst generates a proof for the new theorem
that uses a