Re: [isabelle] Replacing COMP



On Wed, 31 Jul 2013, René Neumann wrote:

And COMP is this THEN variant, is it not?

Not at all. It is just one big misunderstanding. Every time I see remaining occurrences COMP in the Isabelle sources, I need to check several times to convince myself that it is probably right, and not better INCR_COMP or COMP_INCR, or one of the new 8 uniform varieties of the thing that are probably in the next release (for internal use only).

If you want to use Isabelle professionally, you should forget about COMP and do it by more standard means.


Btw: Reading the implementation manual on Drule.compose. It should read "The unique s that unifies ψ and φ_i" (i.e. φ_i and not φ), shouldn't it?

Which implementation manual are you reading excactly? I don't see this in http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf


	Makarius


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