[isabelle-dev] [isabelle] Simplification in locales

[Tobias Nipkow]

> 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.

Tobias