Hi Konrad,
On Thu, Jul 19, 2012 at 7:35 AM, Konrad Slind <[email protected]>wrote:
> > HOL Light just prints them in full, I think. Ah well,
> > as I already wrote, this way of working does not appeal
> > too much to me anyway :-)
> >
> > Freek
>
> It also suffers from the problem that a polymorphic formula
> assumed in this way can't be instantiated. Asserting an axiom
> is more powerful. In HOL4 axiom usage can be tracked in a similar
> way to how assumptions are propagated, so you can get the same
> effect as using an assumption.
>
Could you explain for us relative beginners a bit more what you mean here?
I looked at the HOL Light code for PROVE_HYP, but the meaning and use are
not clear to me.
And anyway I am wondering if you mean that asserting an axiom is more
powerful than _any_ ASSUME-like mechanism, or is somehow specific to
PROVE_HYP.
Additional enlightenment will be much appreciated.
-Cris
>
> Konrad.
>
>
> ------------------------------------------------------------------------------
> 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
