Re: [isabelle] rule_format and locales



Peter Lammich wrote:

I want to use a rule_format transformation for a lemma inside a locale ...

The attribute is only applied inside the locale, not to the exported version (as dummy.X in your example).

It is not recommended to use attributes that undertake heavy theorem transformations inside a locale---for example, simplified. These are executed whenever a context is built from the locale and you will end up with very slow code.

Clemens






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