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 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.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
