# [isabelle] using mono predicate

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] using mono predicate
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Thu, 28 Apr 2011 14:18:25 +0300
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.15) Gecko/20110303 Lightning/1.0b2 Thunderbird/3.1.9

Hello,
I have the following theory fragment:
theory test imports Main
begin
class test = lattice
begin
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.*