Regular expression search for theorem

[mn200]

The function DB.find function does a substring match. Why not extend to allow the string to be a regular expression.

Along the way, we should allow an operator to allow easy search for fragments. Something like

re1 ~~ re2  ==  re1.*re2 | re2.*re1

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.