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
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
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,
This looks like a regression.
Can you turn this into an issue on github please?
Michael
From: Waqar Ahmad via hol-info
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 3 July 2018 at 01:41
To: hol-info
Subject: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12
Hi all,
I
