Hi Ramana, Thank you, it’s perfect. (I replaced FIRST_X_ASSUM with POP_ASSUM in my case)
Regards, Chun > Il giorno 20 gen 2017, alle ore 22:25, Ramana Kumar > <ramana.ku...@cl.cam.ac.uk> ha scritto: > > How about this? first_x_assum(strip_assume_tac o MATCH_MP th) > > On 21 January 2017 at 06:39, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: >> 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 >> >> >> ------------------------------------------------------------------------------ >> 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: 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
