[isabelle] "Full name" of a locale



Hi,

If I want to retrieve the full name of a locale in a theory (by
Sign.full_name?), how do I retrieve the binding? Why does Sign.full_name
need the binding?

Thanks in advance.

Steve




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