  Many facts possess symmetrical counterparts that often require a separate
formal proof, depending on the nature of the involved symmetry. We introduce a
method in Isabelle/HOL which produces such a symmetrical fact for the list
datatype and the symmetry induced by the list reversal mapping. The method is
implemented as an attribute and its result is based on user-declared symmetry
rules. Besides general rules, we provide rules that are aimed to be applied in
the domain of Combinatorics on Words.
