  Formal verification of a software system relies on formalising the
requirements to which it should adhere, which can be challenging. While
formalising requirements from natural-language, we have dependencies that lead
to duplication of information across many requirements, meaning that a change
to one requirement causes updates in several places. We propose to adapt code
refactorings for NASA's Formal Requirements Elicitation Tool (FRET), our
tool-of-choice. Refactoring is the process of reorganising software to improve
its internal structure without altering its external behaviour; it can also be
applied to requirements, to make them more manageable by reducing repetition.
FRET automatically translates requirements (written in its input language
Fretish) into Temporal Logic, which enables us to formally verify that
refactoring has preserved the requirements' underlying meaning. In this paper,
we present four refactorings for Fretish requirements and explain their
utility. We describe the application of one of these refactorings to the
requirements of a civilian aircraft engine software controller, to decouple the
dependencies from the duplication, and analyse how this changes the number of
requirements and the number of repetitions. We evaluate our approach using
Spot, a tool for checking equivalence of Temporal Logic specifications.
