[isabelle-dev] [isabelle] Simplification in locales
nipkow at in.tum.de
Fri Jun 27 22:34:11 CEST 2008
> I agree that the locale abstraction is being violated in this case. Even
> if locale-defined constants are implemented as abbreviations, this
> should not be apparent to the user. Here's my idea for a possible
> remedy: Within the locale, the simplifier should use a congruence rule
> that prevents the implicit parameters from being rewritten:
> lemma f_cong [cong]: "y = z ==> l.f x y = l.f x z"
Well spotted. We have also toyed with this idea but hadn't done anything
about it yet because locales are still not 100% finished.
More information about the isabelle-dev