I just wanted to point out, in case you didn't know, that many tactics have
lowercase synonyms so you don't have to write them out in all capital
letters. For example pop_assum and rewrite_tac.
There are also some cheatsheets around online for commonly used tactics,
e.g., http://sange.fi/~magnus/cheatsheet.txt and
https://gist.github.com/xrchz/71048e26e42f7f195d1726a855a4d2ff. Maybe these
should be linked from the main website (and probably merged)...
On 26 September 2017 at 04:42, Mario Castelán Castro <marioxcc...@yandex.com
> wrote:
> Hello Chun Tian.
>
> On 25/09/17 17:12, Chun Tian (binghe) wrote:
> > To prevent "explicit" lambda expressions in this case, what I've learnt
> > from Joe Hurd is the following simple helper ML function:
> >
> > fun wrap a = [a];
> >
> > then your "POP_ASSUM (fn thm => REWRITE_TAC [thm])" becomes "POP_ASSUM
> > (REWRITE_TAC o wrap)".
>
> Thanks you. This does nicely what I wanted.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> ------------------------------------------------------------
> ------------------
> 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
