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.


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