Yes, indeed. When the subgoals are identical (including the assumptions), Tactical.USE_SG_THEN ACCEPT_TAC should do it.
Otherwise, the doc for USE_SG_THEN gives a couple of examples how it can be used. This requires you to identify which subgoal is to be used in proving which other. They need not be identical. But I guess something could be written to trawl through the list of subgoals looking for pairs where one proves the other without effort (ie, same conclusion, same or subset assumptions) Cheers, Jeremy On 01/02/15 16:46, Ramana Kumar wrote: > Is it possible to merge duplicate (or alpha-convertible) subgoals during > a proof, to reduce the total number of subgoals? Maybe using list tactics? > > > ------------------------------------------------------------------------------ > Dive into the World of Parallel Programming. The Go Parallel Website, > sponsored by Intel and developed in partnership with Slashdot Media, is your > hub for all things parallel software development, from weekly thought > leadership blogs to news, videos, case studies, tutorials and more. Take a > look and join the conversation now. http://goparallel.sourceforge.net/ > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Dive into the World of Parallel Programming. The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
