Re: [isabelle] Replacing COMP



Am 31.07.2013 22:46, schrieb Makarius:
> 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.

I'd like to point out though, that I do not use Isabelle/ML and hence
the point (as I understand you), that using it in ML without thought
might deal some harm, does not apply here. Or could it really deal some
damage in the high-level view I'm using?

I do trust you that there are good reasons to remove COMP. Still my wish
to have those THEN/OF variants remains :)

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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