[isabelle] Bizarre type unification error



In the attached proof script, I receive the following message after
loading the buffer into Isabelle:

*** Type unification failed
*** Type error in application: Incompatible operand type
***
*** Operator:  Cl_P :: 'a set => 'a set
*** Operand:   T :: ??'a llist set
***
*** At command "assume".

I expect these types to be unifiable.  Should not "??'a llist set"
unify with "'a set" such that "??'a llist = 'a"?

I'm attempting to use a set of functions out of which I'm going to
pick an arbitrary function and invoke the only property I know about
it (namely, that it's monotonic; see the definition Cls).  What have I
done wrong?

The proof script depends on the LList2 library, available on AFP
(http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml).

-- 
 Denis

Attachment: Error.thy
Description: Binary data



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