# Reference manual / Z-related commands / Refinement commands / remove invariant

This command is part of the experimental refinement editor.

The remove invariant command refines a specification statement to replace its invariant by true. It applies the following inference rule of the refinement calculus.

 ? P I      ? Q I      ? F[P, Q] ? F[P,I,Q]

No code is implicitly generated by this refinement rule.

The remove invariant command is applicable when a specification statement F[P,I,Q] in a goal is inspected, except where I is already true.

## Tactic example

"remove invariant" p

This example applies the remove invariant command to specification statement p.

IT 20-Nov-2000