Simplify only using one definition

Question

The simplifier (simp) in Isabelle/HOL rewrites by using all the lemmas/theorems/definitions/etc in the system. I know that we can delete a definition from the simplifier. For example, like this:

by (simp del:less_imp_le_nat) 

I need to simplify by only using the lemma set_rec. How can I delete all the theorems in the simplifier and only add the lemma set_rec?

Something like:

by (simp del_all del:set_rec) 

Answer 1

You can use apply(simp only: set_rec).