[opentheory-users] article writers

Ramana Kumar ramana.kumar at gmail.com
Mon Jan 10 23:48:29 UTC 2011


How many proof assistants have article writers? I presume at least
HOL-light does, since it was used to make the standard library
(right?).

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?

Alternatively, there is a logging.ml file in
gilith/opentheory/data/hol-light/, which is certainly useful to read,
but appears to be for creating articles in the old format where there
was still a "call" command. Is the code for writing articles in the
new format available for inspection or copying?



More information about the opentheory-users mailing list