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).
On Wed, Apr 25, 2012 at 12:42 PM, Rob Arthan <[email protected]> wrote:
> Conversations with Mark Adams and John Harrison at the Milner Symposium
> earlier last week inspired me to think through a new approach to defining
> constants in HOL. This generalises what was done in early versions of HOL
> Light. It constitutes an adjustment to new_specification that supersedes
> new_definition altogether and is less restrictive as regards the
> polymorphism of the defining axiom than the existing new_specification.
>
> I would welcome any comments anyone may have on this proposal, which can
> be found at http://www.lemma-one.com/papers/hcddr.pdf. Comments on the
> correctness or otherwise of any of the informal proofs in the proposal
> would be particularly welcome.
>
> Regards,
>
> Rob.
>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
