Named-formulas
Utilities for named formulas.
A named formula is a formula with a name (a symbol).
There are utilities to (attempt to) programmatically prove named formulas,
optionally printing progress messages.
There are also utilities to turn named formulas into theorem event forms,
ensuring the freshness and uniqueness of the theorem names.
Subtopics
- Named-formulas-to-thm-events
- Turn a list of named formulas into theorem events.
- Named-formula-to-thm-event
- Turn a named formula into a theorem event.
- Prove-named-formulas
- Try to prove a list of named formulas, one after the other.
- Prove-named-formula
- Try to prove a named formula.
- Ensure-named-formulas
- Cause a soft error if the proof of any named formula fails.
