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
