Re: [isabelle] locale default structure

> I have some odd(?) behaviour when combining locales:
> Given:
>   locale test = complete_lattice L + complete_lattice FL

> the default index for operators like \<squnion> is L, but the default structure for referencing a lemma is FL.

I now retired to the following locale, where both, the default indexing of operators and the default qualifiyng of theorem names are L.
 locale test = struct L + complete_lattice FL + complete_lattice L

although I have no idea, why this works.

-- Peter Lammich

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