I'd say a big difference is that irule can only be used as a tactic,
whereas MP_CANON is a rule that can be used in more general situations.
Could the technology inside irule be split out into a rule or conversion,
or is it essentially a tactic?
On 17 November 2015 at 00:39, Jeremy Dawson
Hi Ramana,
Well, they are both ways of matching the final consequent of a1 ==> a2
==> a3 ==> ... ==> c with the goal.
Until I saw your question I hadn't been aware of the existence of
MP_CANON.
Possibly the biggest difference is that irule will produce multiple new
subgoals (eg, in the above
What is the difference between irule and (match_mp_tac o MP_CANON)?
I'm more interested in differences in the intended design than in minor
details in the implementation. Which is preferred style? Which should get
more developer time?
Maybe they're actually rather different, but as far as I saw,
