Re: [isabelle] Please make OCaml and Ruby part of the Cygwin distribution

Incidentally, the gmane interface to the mailing list, at for example

is much nicer than the antiquated UI available through sourceforge.


On 26 Apr 2014, at 8:13 am, Makarius <makarius at> wrote:

> On Fri, 25 Apr 2014, Yannick Duchêne (Hibou57) wrote:
>> Le Tue, 22 Apr 2014 21:27:41 +0200, Gottfried Barrow <igbi at> a écrit:
>>> If I hadn't been following the occasional discussions about ML vs. OCaml, such as between you and Mark Adams, I might be complaining about how imperfect ML is, but consistency is everything in logic, so not a complaint enters my mind about Isabelle/ML.
>> Please, do you remember the thread's subject and date? I would be interested in reading it.
> It is about HOL-Zero and Ocaml as unsafe programming language etc.
> A very entangled variant of several related and unrelated threads around this can be seen here on the HOL mailing list:
> Title of the thread: "Re: rigorous axiomatic geometry proof in HOL Light".
>       Makarius


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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