Re: [isabelle] rule_format and locales
Peter Lammich wrote:
I want to use a rule_format transformation for a lemma inside a
locale, but it does not work:
If I have, for example:
consts A :: 'a
B :: 'a
lemma (in dummy) X[rule_format]: "ALL x . A x --> B x" sorry
the lemma will be:
> thm dummy.X
ALL x . A x --> B x [!]
but I expected something like
!! x . A x ==> B x
A ?x ==> B ?x
as I get when using rule_format outside a locale.
If I declare
lemmas (in dummy) XX = X[rule_format]
XX has the expected format !
Can I use something similiar to rule_format that works inside a
locale, or do I have to transform the lemmas "by hand" ?
Greetings and thanks for any hints
This archive was generated by a fusion of
Pipermail (Mailman edition) and