Re: [isabelle] Sublocale, subclass and execution.

> It might be helpful to explain what permanent_interpretation does in terms a sublocale declaration and definitions.

This is one item of my documentation dept.

Here a rough sketch:

permanent_interpretation prefix: expr
  where f = t

One key property is that »t« is parsed in the (approximate) syntactic
context of expr (like mixin equations also).  Let »t'« denote the
internalized term.  Then we have:

  f_def: "f = t'"

permanent_interpretation prefix: expr
  -- ‹with implicit mixin: f_def [symmetric]›

Note that the symmetric of f_def is directly integrated as mixin
equation into the resulting mixin morphisms – there is so separate proof

That's it, in short words.


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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