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:

definition
  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
obligation.

That's it, in short words.

Cheers,
	Florian
-- 

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

Attachment: signature.asc
Description: OpenPGP digital signature



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