Hi all,
There has been an interesting discussion on the OpenTheory mailing list
recently regarding how to simplify the two theorems produced by a type
definition in HOL Light and remove their free variables. The latest message
in the thread, which shows the suggestions by Mario Carneiro can be found
here:
http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html.
I'm cross-posting to this list because I think using Mario's suggestions
would be an improvement to both HOL Light and Opentheory. I hope the
respective authors of those systems might agree and implement the changes,
and that anyone else with an interest might voice their opinion.
Cheers,
Ramana
------------------------------------------------------------------------------
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
