[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

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
  where
    "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
  where
    "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
  where
    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

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>