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