[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.e. the following proof will fail:

lemma (in test) "[|a:carrier L; b:carrier L; c:carrier L|] ==> (a\<squnion>b)\<squnion>c = a\<squnion>(b\<squnion>c)" by (simp only: join_assoc)

if I use the qualified name, L.join_assoc to reference the lemma, the proof works. 

I think this behaviour is somewhat odd, because \<squnion> refers to \<squnion>\<^bsub>L\<^esub>, but join_assoc refers to FL.join_assoc.

(How) Can I change this behaviour and make both, the default index and the default scope of the lemmas refer to L ?

Thanks in advance for any help

  Peter Lammich


Der GMX SmartSurfer hilft bis zu 70% Ihrer Onlinekosten zu sparen!
Ideal für Modem und ISDN: http://www.gmx.net/de/go/smartsurfer

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