On 8/30/2018 7:27 PM, michael.norr...@data61.csiro.au wrote:
I'd be happy to see (1) made as a pull request. (Doing it this way gets the
Travis CI to automatically check it (at least to some extent).)
Thank you (https://github.com/HOL-Theorem-Prover/HOL/commit/f05f730),
I'll just continue issu
I'd be happy to see (1) made as a pull request. (Doing it this way gets the
Travis CI to automatically check it (at least to some extent).)
I agree that (2) is a useful distinction to make.
Michael
On 30/8/18, 23:27, "Fabian Immler" wrote:
Dear HOL4 Developers,
In a recent t
Dear HOL4 Developers,
In a recent thread on this list, Makarius mentioned experiments to load
HOL4 in the Isabelle Prover IDE. I participate in such experiments to
load HOL4 with Isabelle/HOL as kernel.
Anyhow, some of the main obstructions concern references (type 'a ref in
SML).
1) In a
