Classify transformations
Make a distinction between transformations that should be used for interactive proof and transformations that should be used in drivers.
Only show the transformations that should be used for interactive proof in the IDE (add a preferences button for this). Also, classify in categories ? (induction, simplify, split etc)