*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Question about locales*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 23 Sep 2008 11:00:33 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <48D3ADA5.50206@uni-muenster.de>*References*: <48D3ADA5.50206@uni-muenster.de>

Hi Peter,

context L begin interpretation concept1[aa bb] end does not work. Neither does: interpretation L \<subseteq> concept1[aa bb]

Here is an example. Assume that you have a locale for rings (forsimplicity, all operations of the ring are bundled in a singeparameter R):locale ring = fixes R assumes ...and a constructor for polynomials Poly, which takes R to itspolynomial ring. You cannot haveinterpretation ring < ring "Poly R"since the right side is not a locale expression. Instead thecomment suggests the following: extend ringlocale poly_ring = ring + fixes P defines "P == Poly R" and now you can make the interpretation interpretation poly_ring < ring P

Clemens

**References**:**[isabelle] Question about locales***From:*Peter Lammich

- Previous by Date: [isabelle] Help with let expressions
- Next by Date: Re: [isabelle] Partial definitions of datatypes
- Previous by Thread: [isabelle] Question about locales
- Next by Thread: [isabelle] CFP: PSI2009 Perspectives of System Informatics
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list