On Sat, May 12, 2012 at 11:54 PM, John Harrison
<[email protected]>wrote:

> | Does this mean unit lists in HOL Light? :)
> | I'm thinking of adding a check that there are no more than 2^30-1 type
> | variables in the input theorem.
>
> I don't exclude either possibility yet...
>

And what about switching to big integers? (for HOL Zero and/or HOL Light)
I thought HOL Zero might be switching to SML at some point anyway?


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

Reply via email to