On Wed, Jul 18, 2012 at 7:49 PM, Felix Breuer <[email protected]> wrote: > Hi Ramana! > > 2012/7/16 Ramana Kumar <[email protected]> >> >> One way to ameliorate this problem is to compose proofs lazily. >> By that, I mean when you get to a step that's obvious to you, just cheat >> (most proof assistants have some option to make a "tagged" theorem without >> proof). > > > Do you (or anyone) know if there is a way to do this in HOL Light?
Looking at HOL Light's kernel briefly I think the only thing you can do is call new_axiom a lot, which isn't exactly what you want, but could work: make many new_axioms when you're cheating (you could write a tactic that does this for use within a proof script), and check the list of axioms to be sure you haven't cheated after you've filled everything in. > > Thanks! > Felix > > -- > http://www.felixbreuer.net ------------------------------------------------------------------------------ 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
