Thank you, this was perfect! > On Aug 8, 2018, at 2:31 AM, Heiko Becker <hbec...@mpi-sws.org> wrote: > > Hello Dylan, > > There are two ways (I know of) to easily work on subgoals: > > 1) You use the >- symbol and not \\ or THEN as it only applies to the first > subgoal > > 2) You use THENL an give it a list of tactics, where the i-th element the > list is applied to subgoal i. > > Personally, I would recommend using ">-". > > Best regards, > > Heiko > > > On 08/08/2018 07:24 AM, Dylan Melville wrote: >> When a goal is separated into multiple subgoals during a proof of the form >> >> # prove(thm,tactic);; >> >> >> Where the last tactic is something like >> >> REPEAT CONJ_TAC >> >> Is there a way to specify that the next tactic should be applied to a >> specific subgoal? In the proof I’m working on, it was applied to all >> subgoals. >> >> >> ------------------------------------------------------------------------------ >> 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 > > > ------------------------------------------------------------------------------ > 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
------------------------------------------------------------------------------ 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
