[opentheory-users] error loading article files (again?).

[Michael Norrish]

> On 2 Jul 2015, at 06:57, Joe Leslie-Hurd <joe at gilith.com> wrote:

> However, I can answer your question right now. I do want the
> OpenTheory fork of HOL Light to be as close as possible to the main
> trunk of HOL Light, but there are certain changes that are required to
> export a standard theory library (which is the primary purpose of this
> fork). For example, introducing an explicit set type (A set) rather
> than the predicate (A -> bool) and removing default cases (e.g., PRE 0
> = 0) are necessary to ensure the standard theory library can be used
> in as many environments as possible.

Is it not now our experience that providing an explicit set type actually makes it *harder* to use OpenTheory in both HOL4 and HOL Light?

Michael

________________________________

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.