The call should look like:
DB.match theories pattern-term
where theories is a list of names of theories in which to search for the
pattern-term. If you leave the list empty, it searches in all theories in
the current hierarchy. I think if you give "-" as a the name, it might
search in the current theory.
You can also use print_apropos as an alternative to DB.match [].
On 16 November 2015 at 11:59, shengyu shen <[email protected]> wrote:
> Dear all:
>
> I know that I can search some particular theorem xx with DB.match like
> this :
>
>
> DB.match ["xx"] pattern
>
> but how can I search the set of theorem proved by me in current session ?
>
>
> Shen
>
>
> ------------------------------------------------------------------------------
> Presto, an open source distributed SQL query engine for big data, initially
> developed by Facebook, enables you to easily query your data on Hadoop in a
> more interactive manner. Teradata is also now providing full enterprise
> support for Presto. Download a free open source copy now.
> http://pubads.g.doubleclick.net/gampad/clk?id=250295911&iu=/4140
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Presto, an open source distributed SQL query engine for big data, initially
developed by Facebook, enables you to easily query your data on Hadoop in a
more interactive manner. Teradata is also now providing full enterprise
support for Presto. Download a free open source copy now.
http://pubads.g.doubleclick.net/gampad/clk?id=250295911&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
