Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML

On Wed, 10 Dec 2014, Thomas Sewell wrote:

If you really need to use it, there is a primitive compose operation which is available via compose_tac, Thm.bicompose etc in the ML sources. This avoids some of the normal automation done around the meta-operators.

This belongs to the "do not try it at home" category. The COMP family with its many options and modes is sometimes given as secret advice, but it requires a lot of thinking around it to get it really right. It is easier to stick to the normal way of things around the RS/OF family.

Note that in most situations COMP_INCR or INCR_COMP is actually needed instead of COMP without the increment mode.


           1,122,353 people so far

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.