Macros provided by SOFT.

`defunvar`,
`defsoft`,
`defun2`,
`defund2`,
`defchoose2`,
`defun-sk2`,
`define2`, and
`define-sk2`
are wrappers of existing events
that record function variables and dependencies of functions on them.
They set the stage for `defun-inst` and `defthm-inst`.

`defun-inst` provides the ability to concisely generate functions,
and automatically prove their termination if recursive,
by specifying replacements of function variables.

`defthm-inst` provides the ability to
concisely generate and automatically prove theorems,
by specifying replacements of function variables.

- Defun-inst
- Introduce a function by instantiating a second-order functions.
- Defequal
- Introduce an equality between functions.
- Defsoft
- Record an existing function as second-order.
- Defthm-inst
- Introduce a theorem by instantiating a second-order theorem.
- Defun2
- Introduce a second-order function
via a second-order version of
`defun`. - Defunvar
- Introduce a function variable.
- Defun-sk2
- Introduce a second-order function
via a second-order version of
`defun-sk`. - Defchoose2
- Introduce a second-order function
via a second-order version of
`defchoose`. - Defthm-2nd-order
- Introduce a second-order theorem.
- Define-sk2
- Introduce a second-order function
via a second-order version of
`std::define-sk`. - Defund-sk2
- Introduce a second-order function
via a second-order version of
`ACL2::defund-sk`. - Define2
- Introduce a second-order function
via a second-order version of
`define`. - Defund2
- Introduce a second-order function
via a second-order version of
`defund`.