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

Is that really necessary?



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