Hi Ramana, >In HOL4 that is called PROVE_HYP.
In HOL Light too, thanks for answering my question! (Its arguments have the opposite order from the function I wrote though :-)) >In HOL4 you can control how much assumptions are printed >with a trace called "assumptions", 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 ------------------------------------------------------------------------------ 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
