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:

  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


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