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:

labelAuth =
 label: lattice
   where le = lblle and lt = lbllt and inf = lblinf and sup = lblsup +
 auth: lattice


Quoting Alexander Krauss <krauss at>:

Hi Randy,

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