It really looks a promising new tool for metamath addicted :-) A couple of remarks:
- I have to input '-cn->' to find -cn-> related theorems - if I input limCC '-cn->' the search engine works in AND (cool!) but the top few results don't contain limCC (I have to scroll down a bit to find theorems containing both constants; but those theorems are actually relevant!) If you are going to tweak it a bit, and maybe add the advanced search feature you mention, it's definitely going to be a tool I will use a lot. Glauco p.s. I use regular expression search with labels a lot, you may consider adding it to the "advanced search" mode; for instance lemul\w* finds a lot of useful theorems focused on <_ and x. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2683fd9f-862a-4244-9328-8c1403c24ccd%40googlegroups.com.
