Re: [isabelle] Combining locales?



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

Alex






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.