Bundling `simp` lemmas?

Stream: Is there code for X?

[Liam Schilling]

Is there an effective structure I can use which allows me to pass a bunch of lemmas to simp as one term?

Specifically, say I know that lemmas A, B, and C will be used together in simp very often. Is there some way I can define myLemmasABC such that simp [myLemmasABC] has the same effect as simp [A, B, C]?

[Notification Bot]

This topic was moved here from #Is there code for X? > Bundling `simp` lemmas by Liam Schilling.

[Chris Henson]

Maybe you are looking for Simp sets?

[Liam Schilling]

Thank you :+1: !