[opentheory-users] article reader for HOL4

Joe Hurd joe at gilith.com
Mon Jan 10 18:57:12 UTC 2011


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



More information about the opentheory-users mailing list