[isabelle] Problems with Char_ord



Hallo,

I need a linorder on strings and imported List_lexord and Char_ord for
that purpose. However, when Isabelle tries to process the imports
command, I get the following error:

 Clash of specifications "Misc.ord_prod_inst.less_prod_def" and
"Product_ord.ord_prod_inst.less_prod_def" for constant
"Orderings.ord_class.less"

I suspect that this has something to do with conflicting definitions of
product orderings. The first one seems to come from
Library/Product_ord.thy The second one probably comes from some kind of
file that is imported by the Collection framework, which I use - perhaps
Collections/common/Misc.thy. But how do I fix this?

Cheers,
Manuel





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