Dear all,
I am working in HOL-Light. I am having an equation and on the right side of
equation, I am having Hilbert choice operator (@). How to remove this
Hilbert choice operator. In the result of that, can I get an existential
quantifier.
--
Regards:
Adnan
------------------------------------------------------------------------------
Put Bad Developers to Shame
Dominate Development with Jenkins Continuous Integration
Continuously Automate Build, Test & Deployment
Start a new project now. Try Jenkins in the cloud.
http://p.sf.net/sfu/13600_Cloudbees
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
