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 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:
Title of the thread: "Re: rigorous axiomatic geometry proof in HOL Light".
This archive was generated by a fusion of
Pipermail (Mailman edition) and