[isabelle] using mono predicate


I have the following theory fragment:

theory test imports Main

class test = lattice

theorem test:
  "f x  = (x::'a) ==> mono f ==> f x = x"

When processing the theorem test I get the following error:

*** Type unification failed: Variable 'a::type not of sort order

The predicate mono is defined in class order and class lattice
extends the class order.

Best regards,

Viorel Preoteasa

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