Hi, suppose currently I have a goal with several assumptions:
P ------------- a0 a1 ... A and a theorem th ``A ==> B`` Now I want to replace the last assumption A into B (and remove A), to reach this new status: P ------------- a0 a1 … B I know the usage of POP_ASSUM, ASSUME_TAC, and MP, but how can I combine these tools into a single tactic to execute? (or there’s another more straight way to achieve the same purpose?) Regards, Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
