Thanks Larry and Thomas, that works a treat for my examples! -- Peter On Mon, 2021-02-15 at 10:36 +0000, Lawrence Paulson wrote: > Try this: > > apply (simp flip: ex_simps all_simps) > >