[isabelle-dev] Locale interpretation with mixins

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Jul 22 15:49:17 CEST 2012

Hi Clemens, hi Makarius,

let me continue concerning syntax:

The current syntax in Tools/interpretation_with_defs.ML is just a proof
of concept:

interpretation L inst
    "bar = t"
  defines f is foo

A much better idea could be to give the new defs in a for-clause:

interpretation L inst
  for f :: T
    "foo = f"
    "bar = t"

where the implicit definitions (f) are mentioned in the for-clause.

One could also think about hiding away the full generality of a) from
the user (for which there might be good reasons) and have something like

interpretation L inst
  for f :: T
    f is foo
    t is bar

Or the where clause could be integrated completely into the locale
expression using named syntax:

interpretation L (| f := foo, t := bar |)
  for f :: T



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120722/3795ab5d/attachment.sig>

More information about the isabelle-dev mailing list