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
Which implementation manual are you reading excactly? I don't see this in
This archive was generated by a fusion of
Pipermail (Mailman edition) and