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

 locale dummy
 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
or
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
 Peter Lammich








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