Perhaps SELECT_ELIM_TAC?
On Thu, Apr 10, 2014 at 6:23 AM, Adnan Rashid
<14dphditaras...@seecs.edu.pk>wrote:
> 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
>
>
------------------------------------------------------------------------------
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
