> 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
