<rewrite-command> ::= rewrite <target> [ with [ reversed ] <names> ]
rewrite immune / lemmas with * rewrite conjecture with distributiveLaws
If reversed is present, all named formulas and rewrite rules, whether or not they are active, that can be oriented from right to left into legal rewrite rules are used with that orientation. If reversed is not present, all named rewrite rules and formulas, whether or not they are active, that can be oriented from left to right are used with that orientation. If no <names> are given, all rewrite rules and left-to-right orientable formulas are used.
The second version of the rewrite command rewrites some term in the current conjecture using the rewrite rules obtained as just described.
The rewrite command is typically used to ``open up'' definitions using a set of passive rewrite rules or to undo an application of a rewrite rule. When reversed is present, the named rewrite rules should ordinarily be passive to prevent them from immediately undoing the result of the rewrite command. See also the normalize command.