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



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

  http://article.gmane.org/gmane.comp.mathematics.hol/1605/

is much nicer than the antiquated UI available through sourceforge.

Michael

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

> On Fri, 25 Apr 2014, Yannick Duchêne (Hibou57) wrote:
>
>> Le Tue, 22 Apr 2014 21:27:41 +0200, Gottfried Barrow <igbi at gmx.com> 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:
>
>  http://sourceforge.net/p/hol/mailman/hol-info/thread/E1SN77r-0007Os-05%40mta0.cl.cam.ac.uk/#msg29180495
>
> 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.