[opentheory-users] article writers

[Joe Hurd]

Hi Ramana,

> How many proof assistants have article writers?

So far only HOL Light has a writer.

> However I can't find any OpenTheory related code in the HOL-light
> sources. This could be because I don't know where to look - is it
> there to be found?

I have a git repo that adds proof logging to HOL Light, and tracks the
official HOL Light svn repo to stay current. You can get my fork here:

http://src.gilith.com/hol-light.html

Most of the proof logging infrastructure is in fusion.ml and
opentheory/logging.ml

Cheers,

Joe