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

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".


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