On 26 Jun 2012, at 09:39, Ramana Kumar wrote:
> I think you shouldn't use new_constant and new_definition. Just the latter
> should be enough to create the new constant with its definition. The former
> creates a constant without a definition
>
Correct.
> (it's like new_axiom in that it should be avoided)
>
new_constant wasn't what the OP wanted in the case in point, but the theory
extensions it makes are conservative, i.e., they extend the vocabulary you can
use but don't extend the statements that can be proved that don't involve the
new vocabulary. I see no reason for telling people to avoid new_constant. If
you use new_axiom, the system gives no guarantee that what you have done is
consistent. That problem doesn't arise with new_constant.
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
