Re: [isabelle] locale default structure
> I have some odd(?) behaviour when combining locales:
> 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