Re: [Hol-info] HOL Constant Definition Done Right

[Rob A. <rd...@le...>]

On 25 Apr 2012, at 14:03, Ramana Kumar wrote:

> Looks like interesting conversations. Congratulations on doing such a great job of writing them up! I would be more than happy to fix the relevant OpenTheory importer/exporters if OpenTheory and/or HOL4 and/or HOL Light adopt this proposal.
> 
> One small comment: in the description of the revised new_specification, there is a capital "P" (below the words "the following axiom:") that should probably be lowercase (or else I misunderstood something).
>    
Thanks for the feedback - you are quite right, the "P" should be "p".

Regards,

Rob.