Use Tactical.THEN (or lcsymtacs.>>, which is the same). On 15 November 2015 at 09:03, shengyu shen <[email protected]> wrote:
> Dear all : > > Supposing I have goal G and I prove it with lots of tactics like folowing : > > > g `G`; > e (t1); > e (t2); > e (t3); > > So after I finished proof, I need to use store_thm to manually collecting > all t1,t2,t3... to save the proven theorem. > > Is there any way to automatically collect all these tactics? > > > Shen > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
