Re: [isabelle] Replacing COMP



Am 29/07/2013 22:39, schrieb Makarius:
> Note that Isabelle/ML provides a variety of
> operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
> with some care where this is really required.

Can you give a concrete example where the use of COMP leads to something the
Isabelle user needs to be protected from?

Tobias




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