[Hol-info] Binomial theorem 2

[Robert M. S. <so...@Ma...>]

I've loaded and opened ringTheory.

- is_ring_def;
> val it =
    |- !r.
         is_ring r =
         (!n m. RP r n m = RP r m n) /\ [snip]...

it looks like a ring is some sort of record and that RP is one of the
slots [probably for the product].

When I type in RP it says "unknown identifier".

So my question is [assuming I'm write that this like a C struct or a
Pascal record] where is the treatment of this in HOL exposed [even the
names of the appropriate source files would be welcome]. I don't think I
saw this in the description manual, but I may have missed it.

	Thanks again.

	--Bob Solovay