theory Transformation imports Main begin text_raw {* \section*{Ad-hoc Transformation of Theorems} *} end