Okay, I imagine HOL-Light does the same. Thank you
> On Jul 3, 2018, at 3:36 PM, Mario Xerxes Castelán Castro
> wrote:
>
> Please include the mailing list in your replies. I do not know what you
> are doing. Anyway, this does not look like HOL4. Are you using HOL
> Light? I only know about HOL4
Please include the mailing list in your replies. I do not know what you
are doing. Anyway, this does not look like HOL4. Are you using HOL
Light? I only know about HOL4. Removing the quantifier will usually be
done internally by the subsequent tactic that requires using the
proposition with a speci
An hypothesis of the form “∀x. P” where “x” occurs free in P is stronger
than just “P” (that is, the former entails the later). Many tactics have
built-in specialization, so it depends on what you want to do. Can you
provide more details?
On 03/07/18 14:18, Dylan Melville wrote:
> Is there any tac
Is there any tactical that can take universal quantification off of a
hypothesis like how GEN_TAC does with the goal?
-Dylan
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot
