Re: theorems-from-file redundant?

[Chris Warburton]

Lots of stuff in theorems.rkt and conjectures.rkt is using
(theorem-files), which contains the full filenames of the tip
benchmarks. These files are being read, parsed, etc. which is all
redundant.

I've added (theorem-ids) to tip.rkt, which lists only the end of the
paths: the parts we use for identifying where a symbol has come
from. I'm now switching theorems.rkt and conjectures.rkt to use these.

We can turn an id into a path using (benchmark-file id), but that should
only be necessary in tests (e.g. to verify that the theorem is the right
one, etc.)