Re: [isabelle] Relating class operations and corresponding locale.



I wrote:
>   "ord.rbt_sorted (op <) = rbt_sorted"

On a related note, I was confused that rbt_sorted has a linorder
constraint while being defined in an ord context. This is a
consequence of the setup around

  http://isabelle.in.tum.de/repos/isabelle/file/f5ca4c2157a5/src/HOL/Library/RBT_Impl.thy#l2055

Is that really necessary?

Cheers,

Bertram




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