[isabelle] How to extract the record from a locale?



For example, given a locale like *ring*, I would like to get the type of
its record ('a set (carrier), 'a=>'a=>'a (mult),...), so that I can feed it
into a function that does an algebraic construction on rings.

definition polynomial_ring :: "<ring_record> => <ring_record>"

-Holden



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.