Remove stripping of conjunctions from `irule`

[xrchz]

Extracts from messages on the HOL info mailing list:

I find it annoying that irule produces lots of new subgoals for the hypotheses. Is there a version that doesn't strip all the conjunctions, so they can be worked on together?

I agree about the stripping of conjunctions. My temptation is to just remove that feature entirely; making the user follow up with rpt conj_tac if that’s what they want doesn’t seem much of an imposition.

[mn200]

I'm totally sympathetic to this, but we documented this behaviour in the Kananaskis-11 release. Perhaps we should avoid introducing a backwards incompatibility. We could come up with another name for the behaviour without the strip_conj. What about rule, say?

[xrchz]

No, I think the behaviour and documentation should be updated.

Additional thought: could we change match_mp_tac to be irule without conjunction stripping? Is that a superset of its current behaviour? (and does the backwards incompatibility of reducing failures matter?)