val mythms = [thm1, th2, th3, ..., th20]; fun metis_extra_tac ths = metis_tac (ths@mythms);
... e(metis_extra_tac [...])... On 15 November 2015 at 11:54, shengyu shen <[email protected]> wrote: > Dear all: > > assume that I have proven a large number of theorems, for example , 20, > can I make METIS_TAC to use them without explictly list all of them? > > > 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
