HolBA simpsets

[totorigolo]

The initial discussion happened here.

Here is a short summary:

• We should rename holBACore_ss to HOLBA_CORE_ss, to follow ssfrag naming convention.
• What about creating some common simpsets in HolBA(Core)Simps?
  • (std_ss++holBACore_ss) => std_holba_ss / shc_ss?
  • should we include wordsTheory and/or pred_setTheory?

[andreaslindner]

std_holba_ss sounds nice to me.

I wouldn't include additional theories in those ones.

I cannot foresee a lot of implications, use cases and associated traps of simplification sets with all of this inside. One of them is that you don't like to blowup your goal's and assumptions' expression sizes with all sorts of theorem rewriting everywhere. But we can (and maybe should, just out of curiosity alone) add std_ultimate_chainsaw_holba_ss with all fun simpsets inside, and see how far this goes well. We could add a comment to std_holba_ss to give it the nickname std_scalpel_holba_ss.

[guancio]

Also add to the wiki the simpset that we use often