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