> 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. 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
