Re: [isabelle] Combining locales?
If this resolves the problem, then not only the order of the arguments
of the locale predicate but also the order of the locale parameters
has changed. The latter is, of course, not internal if a class is
used as a locale.
Randy can make the locale expression invariant to such changes by
using named instantiation syntax like this:
where le = lblle and lt = lbllt and inf = lblinf and sup = lblsup +
Quoting Alexander Krauss <krauss at in.tum.de>:
On 11/14/2011 07:40 PM, Florian Haftmann wrote:
I dimly remember that there have been changes in the type class import
hierarchy which changed the order of arguments for locale predicates,
but I can't recall exactly which. Maybe somebody else can comment?
The change was 5e51075cbd97, and here is the NEWS entry:
* Added syntactic classes "inf" and "sup" for the respective
constants. INCOMPATIBILITY: Changes in the argument order of the
(mostly internal) locale predicates for some derived classes.
Your definition works again, when lblinf/authinf are moved to the
front. The dependence of the predicate arguments on the specifics of
the hierarchy is a bit unfortunate...
This archive was generated by a fusion of
Pipermail (Mailman edition) and