[opentheory-users] article reader for HOL4

[Michael Norrish]

On 11/01/11 05:18, Joe Hurd wrote:
  
> I recently wrote a paper on the OpenTheory standard library that
> contains some details on this:
  
> http://www.gilith.com/research/papers/stdlib.pdf

Emulating HOL Light numerals in HOL4 will be a pain.  Is there any way we could avoid having to expose numeral representations to each other?

I guess HOL4, red-haired step-child that it is, can special case those constants in any articles that it reads, and also do the appropriate inverse thing when writing its own articles.  What does ProofPower do for numerals?

Presumably this kind of translation will be beyond the capabilities of the meta-datato describe.

Michael