| | | B.3.7 simplify: Simplify Formulas |
simplify
simplify F
: simplify
In proving mode with automatic simplification switched off.
If automatic simplification has been switched off (by use of the command option autosimp="false"), this command may be used to trigger simplification explicitly: simplify simplifies all formulas in the current proof state; simplify F simplifies the formula denoted by label F.
The command applies an external transformation procedure: the resulting formula is logically equivalent to the input formula but not necessarily in a form that the user may consider "simpler".
| | | B.3.7 simplify: Simplify Formulas |