[opentheory-users] article reader for HOL4

[Joe Hurd]

Hi Ramana,

I think we are converging here. I agree that the terminology of
defined and input is potentially confusing, but it is at least
consistent from the point of view of the theory.

> For 2... I think we may just be interpreting our words differently. By
> "axioms" I meant the list of theorems so labelled by opentheory info
> --summary, and these cannot be ignored by a reader - they must be
> provided by the reader for the article to succeed.

I've just checked, and I believe opentheory --summary is correctly
classifying assumptions and axioms according to the definition I gave
you. Please let me know if you find an example where it deviates - I
would treat that as a bug.

Cheers,

Joe